Structures · Algebra
NumberField.IsTotallyReal
A field K is totally real if all of its infinite places are real. In other words,
the image of every ring homomorphism K → ℂ is a subset of ℝ.
- Shape
- One type argument · adds isReal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Rat
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- NumberField.IsTotallyReal.isReal
- NumberField.IsTotallyReal.le_maximalRealSubfield
- NumberField.CMExtension.equivMaximalRealSubfield
- NumberField.IsTotallyReal.ofRingEquiv
- NumberField.IsTotallyReal.mult_eq
- NumberField.IsTotallyReal.nrComplexPlaces_eq_zero
- NumberField.IsCMField.ofCMExtension
- NumberField.IsTotallyReal.maximalRealSubfield_eq_top
- NumberField.IsTotallyReal.of_algebra
- NumberField.IsTotallyReal.finrank
- NumberField.CMExtension.equivMaximalRealSubfield_apply
- NumberField.IsTotallyReal.complexEmbedding_isReal
- NumberField.CMExtension.eq_maximalRealSubfield
- NumberField.isTotallyReal_sup
- NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic
- NumberField.isTotallyReal_iSup
- NumberField.instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic
- NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply
- NumberField.instIsTotallyRealSubtypeMemSubfieldTop
- NumberField.CMExtension.equivMaximalRealSubfield.congr_simp
Ancestors0
No ancestors.