Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-29 20:00 879155bf

View on Github →

feat(*): replace fact(0 < t) with ne_zero (#16145) This has almost fully made things easier, whilst also being easier on the typeclass system (fact can cause many slowdowns). It also allows us to make many things that were not instances before into instances.

Estimated changes

modified theorem char_p.char_is_prime_of_pos
added theorem ne_zero.not_char_dvd
added theorem ne_zero.of_not_dvd
deleted theorem ne_zero.not_char_dvd
deleted theorem ne_zero.of_not_dvd
deleted theorem fact.bit0.pos
deleted theorem fact.bit1.pos
deleted theorem fact.pow.pos
deleted theorem fact.succ.pos
modified theorem fin.coe_of_nat_eq_mod'
modified def fin.of_nat'
modified theorem zmod.card_units_eq_totient
deleted theorem pnat.fact_pos
added theorem zmod.cast_eq_val
modified theorem zmod.int_coe_zmod_eq_iff
modified theorem zmod.nat_abs_val_min_abs_le
modified theorem zmod.nat_cast_comp_val
modified theorem zmod.nat_cast_right_inverse
modified theorem zmod.nat_cast_val
modified theorem zmod.nat_cast_zmod_val
modified theorem zmod.nat_coe_zmod_eq_iff
modified theorem zmod.neg_val'
modified theorem zmod.neg_val
modified theorem zmod.val_add
modified theorem zmod.val_eq_ite_val_min_abs
modified theorem zmod.val_injective
modified theorem zmod.val_int_cast
modified theorem zmod.val_le
modified theorem zmod.val_lt
modified theorem zmod.val_min_abs_def_pos
modified theorem dihedral_group.card
modified theorem dihedral_group.order_of_r
modified theorem quaternion_group.card
modified theorem quaternion_group.order_of_a