Commit 2022-11-17 07:53 bb168510
View on Github →feat(algebra/ne_zero): generalize lemmas (#17477)
Lemmas with reduced typeclass assumptions:
zero_ne_one one_ne_zero two_ne_zero three_ne_zero four_ne_zero ne_zero_of_eq_one
Removed lemmas:
is_R_or_C.two_ne_zero two_ne_zero'
New explicit version lemmas:
zero_ne_one' one_ne_zero' two_ne_zero' three_ne_zero' four_ne_zero'
Renamed lemma:
ne_zero.ne' -> ne_zero.nat_cast_ne
New lemma:
ne_zero.ne'
Most of other diffs are just simply replace @lemma with new explicit lemmas
mathlib4: https://github.com/leanprover-community/mathlib4/pull/577