mathlib
40b09aab - feat(*): small lemmas from the sensitivity formalization (#1352)

Commit
6 years ago
feat(*): small lemmas from the sensitivity formalization (#1352) * feat(set_theory/cardinal): norm_cast attributes and extra lemma * feat(logic/basic): ne.symm_iff * feat(data/fin): succ_ne_zero * feat(data/bool): bxor_of_ne * feat(algebra/big_operators, data/fintype): {finset,fintype}.card_eq_sum_ones * feat(data/set): range_restrict * feat(data/finset): inter lemmas * Reid's corrections * fixes * fix cardinal power lemma * fixes * Update bool.lean
Author
Committer
Parents
Loading