Commit 2022-11-17 11:12 a72f0253

View on Github →

feat: synchronize with mathlib3 #17477 (#577) mathlib3: https://github.com/leanprover-community/mathlib/pull/17477

Estimated changes

added theorem NeZero.ne'
added theorem four_ne_zero'
added theorem four_ne_zero
added theorem ne_zero_of_eq_one
added theorem one_ne_zero'
added theorem one_ne_zero
added theorem three_ne_zero'
added theorem three_ne_zero
added theorem two_ne_zero'
added theorem two_ne_zero
added theorem zero_ne_one'
added theorem zero_ne_one