Commit 2024-01-06 14:22 47ca2853

View on Github →

feat: c • x = 0 ↔ c = 0 and similar lemmas (#9390) and rename and generalise smul_eq_zero_iff_eq'/smul_ne_zero_iff_ne' From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Module/Basic.lean

added theorem smul_eq_zero_iff_left

added theorem smul_eq_zero_iff_right

added theorem smul_ne_zero_iff_left

added theorem smul_ne_zero_iff_right

Modified Mathlib/GroupTheory/GroupAction/Group.lean

deleted theorem smul_eq_zero_iff_eq'

deleted theorem smul_ne_zero_iff_ne'

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean