Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-22 15:27 40b09aab

View on Github →

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

Estimated changes

added theorem bool.bxor_iff_ne
added theorem fin.succ_ne_zero
added theorem set.range_restrict
added theorem ne_comm
modified theorem cardinal.nat_cast_inj
modified theorem cardinal.nat_cast_le
modified theorem cardinal.nat_cast_lt
modified theorem cardinal.nat_cast_pow
modified theorem cardinal.nat_succ