Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-19 21:51 faed3a7f

View on Github →

feat(algebra/group_with_zero): slightly generalise mul_ne_zero (#16137) Also tidies a couple of adjacent declarations in the file.

Estimated changes

modified theorem eq_zero_of_mul_self_eq_zero
modified theorem mul_self_ne_zero
modified theorem zero_ne_mul_self