Structures · Algebra
NumberField.IsCMField
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
- Shape
- One type argument · adds to_isTotallyComplex, is_quadratic
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by50
- NumberField.IsCMField.complexConj
- NumberField.IsCMField.unitsMulComplexConjInv
- NumberField.IsCMField.unitsComplexConj
- NumberField.IsCMField.realFundSystem
- NumberField.IsCMField.equivInfinitePlace
- NumberField.IsCMField.ringOfIntegersComplexConj
- NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff
- NumberField.IsCMField.indexRealUnits_mul_eq
- NumberField.IsCMField.complexEmbedding_complexConj
- NumberField.IsCMField.units_rank_eq_units_rank
- NumberField.IsCMField.exists_isConj
- NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion
- NumberField.IsCMField.isConj_complexConj
- NumberField.IsCMField.zpowers_complexConj_eq_top
- NumberField.IsCMField.regOfFamily_realFunSystem
- NumberField.IsCMField.complexConj_apply_apply
- NumberField.IsCMField.complexConj_torsion
- NumberField.IsCMField.closure_realFundSystem_sup_torsion
- NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd
- NumberField.IsCMField.isConj_eq_isConj
- NumberField.IsCMField.map_unitsMulComplexConjInv_torsion
- NumberField.IsCMField.complexConj_ne_one
- NumberField.IsCMField.coe_ringOfIntegersComplexConj
- NumberField.IsCMField.complexConj_eq_self_iff
- NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace
- NumberField.IsCMField.unitsMulComplexConjInv_apply
- NumberField.IsCMField.unitsComplexConj_torsion
- NumberField.IsCMField.unitsMulComplexConjInv_ker
- NumberField.IsCMField.equivInfinitePlace_symm_apply
- NumberField.IsCMField.equivInfinitePlace_apply
- NumberField.IsCMField.orderOf_complexConj
- NumberField.IsCMField.unitsComplexConj_eq_self_iff
- NumberField.IsCMField.ringOfIntegersComplexConj.congr_simp
- NumberField.IsCMField.indexRealUnits_eq_two_iff
- NumberField.IsCMField.realFundSystem.congr_simp
- NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv
- NumberField.IsCMField.complexConj.congr_simp
- NumberField.IsCMField.to_isTotallyComplex
- NumberField.IsCMField.infinitePlace_complexConj
- NumberField.IsCMField.isTotallyComplex
- NumberField.IsCMField.complexConj_apply_eq_self
- NumberField.IsCMField.indexRealUnits_eq_one_or_two
- NumberField.IsCMField.unitsMulComplexConjInv.congr_simp
- NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff
- NumberField.IsCMField.starRing
- NumberField.IsCMField.equivInfinitePlace.congr_simp
- NumberField.IsCMField.is_quadratic
- NumberField.IsCMField.unitsComplexConj.congr_simp
- NumberField.IsCMField.isQuadraticExtension
- NumberField.IsCMField.Units.complexConj_eq_self_iff
Ancestors0
No ancestors.