English
There is a canonical linear isomorphism between the integer-span of a and the quotient of ℤ by the ideal generated by the order of a.
Русский
Существует каноническое линейное изоморфизм между ℤ∗-spаном элемента a и фактор-модулем ℤ/ Ideal.span{order(a)}.
LaTeX
$$$(\mathbb{Z} \cdot a) \cong \mathbb{Z} / \mathrm{Ideal}.span\{\mathrm{addOrderOf}(a)\}$$$
Lean4
/-- The `ℤ`-submodule spanned by a single element `a` is isomorphic to the quotient of `ℤ`
by the ideal generated by the order of `a`. -/
@[simps!]
noncomputable def intSpanEquivQuotAddOrderOf (a : A) : (ℤ ∙ a) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {(addOrderOf a : ℤ)} :=
LinearEquiv.ofEq _ _ (LinearMap.span_singleton_eq_range ℤ A a) ≪≫ₗ
(LinearMap.quotKerEquivRange <| LinearMap.toSpanSingleton ℤ A a).symm ≪≫ₗ
Submodule.quotEquivOfEq _ _
(by
ext1 x
rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
LinearMap.toSpanSingleton_apply])
