English
If M is CancelCommMonoidWithZero and UniqueFactorizationMonoid and NormalizationMonoid and IsMulTorsionFree of its unit group, then M is IsMulTorsionFree.
Русский
Если M — CancelCommMonoidWithZero и UniqueFactorizationMonoid и NormalizationMonoid, и у группы единиц M существует IsMulTorsionFree, то и M является IsMulTorsionFree.
LaTeX
$$$\Bigl[\text{CancelCommMonoidWithZero } M,\ \text{UniqueFactorizationMonoid } M,\ \text{NormalizationMonoid } M,\ \text{IsMulTorsionFree } M^\times\Bigr] \Rightarrow \text{IsMulTorsionFree } M$$$
Lean4
instance : IsMulTorsionFree M := by
refine .mk' fun x hx y hy n hn hxy ↦ ?_
obtain ⟨u, hu⟩ : Associated x y :=
by
have := (Associated.of_eq hxy).normalizedFactors_eq
rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn, ←
associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val, Units.val_eq_one,
IsMulTorsionFree.pow_eq_one_iff hn] at hxy
rwa [hxy, Units.val_one, mul_one] at hu
