Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_self_ne_zero

Modification history

2022-11-11 04:41
src/algebra/group_with_zero/basic.lean
refactor(*): simplifying import hierarchy up to dat.rat.order (#17435) …
Modified mul_self_ne_zeroView on Github →
2022-08-19 21:51
src/algebra/group_with_zero/basic.lean
feat(algebra/group_with_zero): slightly generalise mul_ne_zero (#16137) …
Modified mul_self_ne_zeroView on Github →
2022-04-22 20:06
src/algebra/group_with_zero/basic.lean
chore(*): use zero_lt_two/two_ne_zero lemmas more (#13609)
Added mul_self_ne_zeroView on Github →