English
The integer span of the basis of IsMaxRank coincides with the image of the unit-logs under logEmbedding: span_Z(basisOfIsMaxRank hu) equals map logEmbedding of closure of generated units.
Русский
Целочисленный линейный замык_basisOfIsMaxRank совпадает с образом логарифмов единиц через logEmbedding: span_Z(basisOfIsMaxRank hu) совпадает с image логарифмов через logEmbedding.
LaTeX
$$$\\text{span\_basisOfIsMaxRank}(hu) : \\; \\mathrm{span}_{\\mathbb{Z}}(\\{\\text{basisOfIsMaxRank}(hu)_i\\}) = \\mathrm{AddSubgroup.map}(\\mathrm{logEmbedding}\\,K)(\\mathrm{closure}(\\{u_i\\}))$$$
Lean4
theorem span_basisOfIsMaxRank {u : Fin (rank K) → (𝓞 K)ˣ} (hu : IsMaxRank u) :
(span ℤ (Set.range (basisOfIsMaxRank hu))).toAddSubgroup =
AddSubgroup.map (logEmbedding K) (Subgroup.closure (Set.range u)).toAddSubgroup :=
by
rw [Subgroup.toAddSubgroup_closure, AddMonoidHom.map_closure, ← span_int_eq_addSubgroupClosure]
congr; ext; simp
