index_unitsMulComplexConjInv_range_dvd

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

Похожие утверждения