Theorems · Inductive type · number theory
NumberField.IsTotallyReal
(K : Type u_1) → [Field K] → Prop
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 ℝ.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement · cited by 7,404
Cited by24
Results whose statement or proof uses this declaration.
- NumberField.IsTotallyReal.isRealstatement and proof · cited by 7
- NumberField.CMExtension.equivMaximalRealSubfieldstatement and proof · cited by 3
- NumberField.IsTotallyReal.le_maximalRealSubfieldstatement and proof · cited by 3
- NumberField.nrComplexPlaces_eq_zero_iffstatement · cited by 2
- NumberField.IsTotallyReal.mult_eqstatement and proof · cited by 2
- NumberField.IsTotallyReal.ofRingEquivstatement and proof · cited by 2
- NumberField.CMExtension.equivMaximalRealSubfield_applystatement and proof · cited by 1
- NumberField.isTotallyReal_iff_le_maximalRealSubfieldstatement and proof · cited by 1
- NumberField.isTotallyReal_iff_ofRingEquivstatement and proof · cited by 1
- NumberField.isTotallyReal_top_iffstatement · cited by 1
- NumberField.IsCMField.ofCMExtensionstatement and proof · cited by 1
- NumberField.IsTotallyReal.casesOnstatement and proof · cited by 1