English
A precise dichotomy: indexRealUnits(K) is 1 or 2; the exact value corresponds to whether the CM-field contributes an extra independent real unit beyond the real subfield.
Русский
Точное дихотомическое утверждение: indexRealUnits(K) равно 1 или 2; точное значение соответствует тому, имеет ли CM-поле дополнительную независимую вещественную единицу помимо реального подполя.
LaTeX
$$$$ \\operatorname{indexRealUnits}(K) = 1 \\lor \\operatorname{indexRealUnits}(K) = 2 $$$$
Lean4
theorem indexRealUnits_mul_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2 :=
by
rw [indexRealUnits, sup_comm]
convert (Subgroup.index_map (torsion K) (unitsMulComplexConjInv K)).symm
· rw [unitsMulComplexConjInv_ker]
· rw [map_unitsMulComplexConjInv_torsion, IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right]
rw [Nat.card_eq_fintype_card]
exact even_iff_two_dvd.mp (even_torsionOrder K)
