English
Let A be a subgroup of an additive group M that is also an R-module. Given an R-basis b of M and a witness h asserting A equals the closure of the range of b, one can transport this basis to define a Basis of A over the integers ℤ via restriction of scalars from R to ℤ followed by an isomorphism to A.
Русский
Пусть A — подгруппа аддитивной группы M, также модуль над R. Для базиса R-модуля M и свидетельства h, что A есть замыкание образа b, можно перенести этот базис и получить базис над ℤ для A через ограничение скаляров и изоморфизм с A.
LaTeX
$$$\\text{addSubgroupOfClosure}(A,b,h) : Basis\\ ι\\ \\mathbb{Z}\\ A^{\\mathrm{toIntSubmodule}}$$$
Lean4
/-- Let `A` be an subgroup of an additive commutative group `M` that is also an `R`-module.
Construct a basis of `A` as a `ℤ`-basis from a `R`-basis of `E` that generates `A`.
-/
noncomputable def addSubgroupOfClosure (h : A = .closure (Set.range b)) : Basis ι ℤ A.toIntSubmodule :=
(b.restrictScalars ℤ).map <|
LinearEquiv.ofEq _ _ (by rw [h, ← Submodule.span_int_eq_addSubgroupClosure, toAddSubgroup_toIntSubmodule])
