Theorems · Inductive type · number theory
NumberField.IsCMField
(K : Type u_1) → [inst : Field K] → [CharZero K] → Prop
A field K is CM if K is a totally complex quadratic extension of its maximal
real subfield K⁺.
- Defined in
- Mathlib.NumberTheory.NumberField.CMField
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by53
Results whose statement or proof uses this declaration.
- NumberField.IsCMField.complexConjstatement and proof · cited by 14
- NumberField.IsCMField.unitsMulComplexConjInvstatement and proof · cited by 9
- NumberField.IsCMField.unitsComplexConjstatement and proof · cited by 5
- NumberField.IsCMField.equivInfinitePlacestatement and proof · cited by 4
- NumberField.IsCMField.realFundSystemstatement and proof · cited by 4
- NumberField.IsCMField.ringOfIntegersComplexConjstatement and proof · cited by 3
- NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iffstatement and proof · cited by 2
- NumberField.IsCMField.complexEmbedding_complexConjstatement and proof · cited by 2
- NumberField.IsCMField.exists_isConjstatement and proof · cited by 2
- NumberField.IsCMField.indexRealUnits_mul_eqstatement and proof · cited by 2
- NumberField.IsCMField.isConj_complexConjstatement and proof · cited by 2
- NumberField.IsCMField.unitsMulComplexConjInv_apply_torsionstatement and proof · cited by 2