English
If M is a CancelCommMonoidWithZero and, for all nonzero x,y and n ≠ 0, x^n = y^n implies x = y, then M is a multiplicative torsion-free monoid.
Русский
Если M — CancelCommMonoidWithZero и для любых не нулевых x,y и n ≠ 0 выполняется x^n = y^n ends x = y, тогда M является мултипликативно torsion-free.
LaTeX
$$$\text{If }M\text{ is a CancelCommMonoidWithZero and }\forall x,y\,(x\neq 0\land y\neq 0)\,\forall n\,(n\neq 0),\ (x^n = y^n) \Rightarrow x=y,\text{ then }M\text{ is IsMulTorsionFree } M$.$$
Lean4
theorem mk' (ih : ∀ x ≠ 0, ∀ y ≠ 0, ∀ n ≠ 0, (x ^ n : M) = y ^ n → x = y) : IsMulTorsionFree M :=
by
refine ⟨fun n hn x y hxy ↦ ?_⟩
by_cases h : x ≠ 0 ∧ y ≠ 0
· exact ih x h.1 y h.2 n hn hxy
grind [pow_eq_zero, zero_pow]
