Theorem right_ne_zero_of_smul

Modification history

2024-02-06 20:37
Mathlib/Algebra/SMulWithZero.lean
feat: HahnSeries smul order inequality (#9848) …
Modified right_ne_zero_of_smulView on Github →
2024-01-07 19:34
Mathlib/Algebra/SMulWithZero.lean
chore(*): replace `$` with `<|` (#9319) …
Modified right_ne_zero_of_smulView on Github →
2023-01-25 10:47
Mathlib/Algebra/SMulWithZero.lean
feat: `a • b ≠ 0 → b ≠ 0` (#1411) …
Added right_ne_zero_of_smulView on Github →