English
If an abelian group A is divisible by integers (i.e. for every n ∈ ℤ⁺ there exists b with nb = a for any a ∈ A), then A is a Baer module over ℤ.
Русский
Если абеллова группа A делима на целые числа, то она является модулем Баера над ℤ.
LaTeX
$$$ \\mathrm{DivisibleBy}(A, \\mathbb{Z}) \\Rightarrow \\mathrm{Module.Baer}(\\mathbb{Z}, A) $$$
Lean4
theorem of_divisible [DivisibleBy A ℤ] : Module.Baer ℤ A := fun I g ↦
by
rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩
obtain rfl | h0 := eq_or_ne m 0
· refine ⟨0, fun n hn ↦ ?_⟩
rw [Submodule.span_zero_singleton] at hn
subst hn
exact (map_zero g).symm
let gₘ := g ⟨m, Submodule.subset_span (Set.mem_singleton _)⟩
refine ⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩
rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩
rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g, SetLike.mk_smul_mk]
