Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-12 20:05 fb7dfa16

View on Github →

feat(data/{nat,int,zmod,finset}): add a few useful facts (#1220)

  • feat(data/finset): add a few useful facts
  • feat(data/zmod/basic): express neg in terms of residues
  • feat(data/{nat,int}): add theorem 'mod_mod_of_dvd'

Estimated changes

added theorem finset.bind_inter
added theorem finset.filter_insert
added theorem finset.filter_inter
added theorem finset.inter_bind
added theorem finset.inter_filter
added theorem finset.inter_sdiff
modified theorem int.mod_mod
added theorem int.mod_mod_of_dvd
added theorem nat.mod_mod_of_dvd
added theorem zmod.neg_val'
added theorem zmod.neg_val