English
For a CM-field K, the fundamental system of units of the maximal real subfield K^+ can be canonically viewed as a family of units in the ring of integers of K; that is, there is a function realFundSystem: Fin(rank K) → (\\mathcal{O}_K)^× sending each index to the corresponding unit obtained by transporting a fundamental system from K^+ to K.
Русский
Для поля CM K фундаментальная система единиц максимального действительного подполя K^+ может быть канонически воспринята как семейство единиц в кольце целых O_K; то есть существует отображение realFundSystem: Fin(rank K) → (O_K)^×, отправляющее каждый индекс в соответствующую единицу, полученную перенесением фундаментальной системы из K^+ в K.
LaTeX
$$$\\text{realFundSystem}: \\mathrm{Fin}(\\mathrm{rank}\\,K) \\to (\\mathcal{O}_K)^{\\times}$$$
Lean4
/-- The fundamental system of units of `K⁺` as a family of `(𝓞 K)ˣ`.
-/
noncomputable def realFundSystem : Fin (rank K) → (𝓞 K)ˣ := fun i ↦
(Units.map (algebraMap (𝓞 K⁺) (𝓞 K)).toMonoidHom) (fundSystem K⁺ (finCongr (units_rank_eq_units_rank K).symm i))
