Theorems · Inductive type · field theory
IsRealClosed
(R : Type u_1) → [Field R] → Prop
A field R is real closed if all of the following hold:
1. R is real (that is, -1 is not a sum of squares in R).
2. for every x in R, one of x or -x is a square.
3. every odd-degree polynomial over R has a root in R.
- Defined in
- Mathlib.FieldTheory.IsRealClosed.Basic
- Cited by
- 13 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 by15
Results whose statement or proof uses this declaration.
- IsRealClosed.isSquare_or_isSquare_negstatement and proof · cited by 4
- IsRealClosed.exists_eq_pow_of_isSquarestatement and proof · cited by 2
- IsRealClosed.exists_eq_pow_of_oddstatement and proof · cited by 2
- IsSquare.of_nonnegstatement and proof · cited by 2
- IsRealClosed.exists_eq_zpow_of_isSquarestatement and proof · cited by 1
- IsRealClosed.exists_isRoot_of_odd_natDegreestatement and proof · cited by 1
- IsRealClosed.nonneg_iff_isSquarestatement and proof · cited by 1
- IsRealClosed.casesOnstatement and proof · cited by 0
- IsRealClosed.exists_eq_pow_of_nonnegstatement and proof · cited by 0
- IsRealClosed.exists_eq_zpow_of_nonnegstatement and proof · cited by 0
- IsRealClosed.exists_eq_zpow_of_oddstatement and proof · cited by 0
- IsRealClosed.isSquare_neg_of_not_isSquarestatement and proof · cited by 0