Theorems · Theorem · number theory

NumberField.IsCMField.indexRealUnits_eq_two_iff

∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.IsCMField.indexRealUnits K = 2 ↔
    ∃ u, Subgroup.zpowers ((NumberField.IsCMField.unitsMulComplexConjInv K) u) = ⊤

The index of the subgroup of (𝓞 K)ˣ generated by the real units and the roots of unity is equal to 2 iff there exists a unit whose image by unitsMulComplexConjInv generates the torsion subgroup of K.

Defined in

Mathlib.NumberTheory.NumberField.CMField

Cited by

0 results in Mathlib

Foundations

Depth 314 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCharZeroNumberField.IsCMFieldNumberField