Documentation

Mathlib.Data.Real.CompleteField

The reals are a conditionally complete linearly ordered field #

source
noncomputable instance instConditionallyCompleteLinearOrderedFieldReal :
ConditionallyCompleteLinearOrderedField ℝ

The reals are a conditionally complete linearly ordered field.

Equations
    source
    instance Real.RingHom.unique :
    Unique (ℝ →+* ℝ)

    There exists no nontrivial ring homomorphism ℝ →+* ℝ.

    Equations