Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.forall_mem_insert_eq

Modification history

2017-08-27 13:33
data/finset/basic.lean
refactor(data/finset): add type class instances
Deleted finset.forall_mem_insert_eqView on Github →
2017-08-27 13:33
data/finset/basic.lean
feat(data/finset): add basics for finsets
Added finset.forall_mem_insert_eqView on Github →
2017-08-26 13:03
data/finset/basic.lean
refactor(data/finset): add type class instances
Deleted finset.forall_mem_insert_eqView on Github →
2017-08-25 13:00
data/finset/basic.lean
refactor(data/finset): fix formatting issues
Added finset.forall_mem_insert_eqView on Github →
2017-08-24 19:09
data/finset/basic.lean
feat(topology): add topological structures for groups, ring, and linear orders; add instances for rat and real
Deleted finset.forall_mem_insert_eqView on Github →
2017-08-24 16:21
data/finset/basic.lean
feat(data/finset): add basics for finsets
Added finset.forall_mem_insert_eqView on Github →