Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 10:43 3996bd42

View on Github →

chore(logic/basic): add a few simp lemmas (#5278) Also add fintype.prod_eq_single.

Estimated changes

Modified archive/arithcc.lean

Modified src/data/fintype/card.lean

added theorem fintype.prod_eq_single

Modified src/data/matrix/basic.lean

Modified src/logic/basic.lean

added theorem decidable.not_imp_self

added theorem imp_not_self

added theorem ite_eq_left_iff

added theorem ite_eq_right_iff

added theorem not_imp_self

Modified src/ring_theory/power_series.lean