Documentation

HexRealRootsTheory.RealClosed

Imports

Init
Mathlib.Analysis.Polynomial.Order
Mathlib.Analysis.Real.Sqrt
Mathlib.FieldTheory.IsRealClosed.Basic

Imported by

Real.instIsRealClosed

instance Real.instIsRealClosed :

IsRealClosed ℝ

The real numbers form a real closed field.