mathlib
faed3a7f - feat(algebra/group_with_zero): slightly generalise mul_ne_zero (#16137)

Commit

3 years ago

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

Author

ericrbg

Parents