English
The indexRealUnits of the group of units equals the index of the subgroup generated by real units and torsion, yielding a factor of 2 when CM-field structure is present.
Русский
Индекс realUnits равен индексу подгруппы, порождаемой вещественными единицами и torsion, что даёт множитель 2 при CM-паре.
LaTeX
$$$$ \\operatorname{indexRealUnits}(K) \\cdot \\operatorname{index}( (unitsMulComplexConjInv K).range ) = 2 $$$$
Lean4
/-- The index of the image of `unitsMulComplexConjInv` divides `2`.
-/
theorem index_unitsMulComplexConjInv_range_dvd : (unitsMulComplexConjInv K).range.index ∣ 2 :=
by
suffices (powMonoidHom 2 : _ →* torsion K).range.index = 2
by
refine this ▸ Subgroup.index_dvd_of_le ?_
rintro _ ⟨ζ, _, rfl⟩
exact ⟨ζ, Subtype.ext_iff.mpr (by simp [pow_two])⟩
rw [IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right_iff_dvd, Nat.card_eq_fintype_card]
exact Even.two_dvd <| even_torsionOrder K