Mathlib Changelog
v4
Changelog
About
Github
Theorem
left_ne_zero_of_smul
Modification history
2025-03-05 10:07
Mathlib/Algebra/GroupWithZero/Action/Defs.lean
chore: move `SMulWithZero` with `SMulZeroClass` (#13027) …
Modified
left_ne_zero_of_smul
View on Github →
2023-12-30 21:45
Mathlib/Algebra/SMulWithZero.lean
chore(*): drop `$`/`<|` before `fun` (#9361) …
Modified
left_ne_zero_of_smul
View on Github →
2023-01-25 10:47
Mathlib/Algebra/SMulWithZero.lean
feat: `a • b ≠ 0 → b ≠ 0` (#1411) …
Added
left_ne_zero_of_smul
View on Github →