Theorem smul_eq_zero_iff_eq'

Modification history

2026-10-10 12:26

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors (#40604) …

Added smul_eq_zero_iff_eq'View on Github →

2024-01-06 14:22

Mathlib/GroupTheory/GroupAction/Group.lean

feat: `c • x = 0 ↔ c = 0` and similar lemmas (#9390) …

Deleted smul_eq_zero_iff_eq'View on Github →

2022-12-22 16:23

Mathlib/GroupTheory/GroupAction/Group.lean

feat port: GroupTheory.GroupAction.Group (#1146)

Added smul_eq_zero_iff_eq'View on Github →