English
The image of realUnits under the inclusion into units of the ring of integers matches the subgroup described by the torsion-division interactions with conj; in particular, the range of realUnits coincides with a fixed 2-divisible subgroup.
Русский
Образ realUnits через включение в единицы кольца целых совпадает с заданной подгруппой, связанной с взаимодействием torsion и сопряжения; в частности, образ равен фиксированной 2-разделимой подгруппе.
LaTeX
$$$$ \\mathrm{range}( \\mathrm{realUnits}(K) ) = \\mathrm{range}( \\text{algebraMap}_{K^+\\to K} ) $$$$
Lean4
/-- The index of the subgroup of `(𝓞 K)ˣ` generated by the real units and the roots of unity is
equal to `1` or `2` (see `NumberField.IsCMField.indexRealUnits_eq_two_iff` for the computation
of this index).
-/
theorem indexRealUnits_eq_one_or_two : indexRealUnits K = 1 ∨ indexRealUnits K = 2 :=
by
have h₁ := indexRealUnits_mul_eq K
obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K
· exact Or.inr <| by rwa [h₂, mul_one] at h₁
· exact Or.inl <| by rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁
