English
If left multiplication by k is injective on G, then k • a = k • b implies a = b.
Русский
Если умножение слева на k инъективно на G, то k • a = k • b ⇒ a = b.
LaTeX
$$$ (\forall x \in G)\ k \cdot x = 0 \Rightarrow x = 0 \quad \Rightarrow \quad k \cdot a = k \cdot b \Rightarrow a = b. $$$
Lean4
/-- `smul` by a `k : M` over a group is injective, if `k` is not a zero divisor.
The general theory of such `k` is elaborated by `IsSMulRegular`.
The typeclass that restricts all terms of `M` to have this property is `NoZeroSMulDivisors`. -/
theorem smul_cancel_of_non_zero_divisor {M G : Type*} [Monoid M] [AddGroup G] [DistribMulAction M G] (k : M)
(h : ∀ x : G, k • x = 0 → x = 0) {a b : G} (h' : k • a = k • b) : a = b :=
by
rw [← sub_eq_zero]
refine h _ ?_
rw [smul_sub, h', sub_self]
