English
For an Additive commutative monoid M, M is torsion as an AddMonoid if and only if M is torsion as a ℕ-module; i.e., every element has finite order both additively and as a ℕ-module action.
Русский
Для аддитивного коммутативного моноида M выполняется эквивалентность: M торсион по операции сложения как AddMonoid эквивалентно тому, что M торсион как модуль над ℕ; то есть каждый элемент имеет конечный порядок как по сложению, так и под действием ℕ.
LaTeX
$$$\\text{AddMonoid.IsTorsion}(M) \\iff \\text{Module.IsTorsion } \\mathbb{N} \\ M$$$
Lean4
theorem isTorsion_iff_isTorsion_nat [AddCommMonoid M] : AddMonoid.IsTorsion M ↔ Module.IsTorsion ℕ M :=
by
refine ⟨fun h x => ?_, fun h x => ?_⟩
· obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩
· rw [isOfFinAddOrder_iff_nsmul_eq_zero]
obtain ⟨n, hn⟩ := @h x
exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩
