Commit 2022-11-11 04:19 d88e5423

View on Github →

feat: port Algebra.NeZero (#557) The lemmas coe_trans and trans were removed (see zulip discussion).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/NeZero.lean

added theorem NeZero.ne

added theorem NeZero.of_pos

added theorem eq_zero_or_neZero

added theorem neZero_iff

added theorem not_neZero