mathlib
12c24b79 - feat(algebra/smul_with_zero): `a • b ≠ 0 → a ≠ 0` (#18086)

Commit

2 years ago

feat(algebra/smul_with_zero): `a • b ≠ 0 → a ≠ 0` (#18086) This matches existing `mul` lemmas

Author

YaelDillies

Parents