The reals are a conditionally complete linearly ordered field

noncomputable instance instConditionallyCompleteLinearOrderedFieldReal : ConditionallyCompleteLinearOrderedField ℝ

The reals are a conditionally complete linearly ordered field.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Real.RingHom.unique = { default := RingHom.id ℝ, uniq := Real.RingHom.unique.proof_1 }