Theorems · Theorem · number theory
NumberField.IsCMField.indexRealUnits_eq_one_or_two
∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] [NumberField K], NumberField.IsCMField.indexRealUnits K = 1 ∨ NumberField.IsCMField.indexRealUnits K = 2
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).
- Defined in
- Mathlib.NumberTheory.NumberField.CMField
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 314 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- mul_oneproof · cited by 3,885
- CharZerostatement and proof · cited by 932
- NumberFieldstatement and proof · cited by 653
- MonoidHom.rangeproof · cited by 314
- two_ne_zeroproof · cited by 251
- Subgroup.indexproof · cited by 150
- Nat.prime_twoproof · cited by 55
- NumberField.IsCMFieldstatement and proof · cited by 45
- Nat.dvd_primeproof · cited by 18
- NumberField.IsCMField.unitsMulComplexConjInvproof · cited by 9
- NumberField.IsCMField.indexRealUnitsstatement and proof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.