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_2 }

@[simp]

theorem Real.ringHom_apply {F : Type u_1} [FunLike F ℝ ℝ] [RingHomClass F ℝ ℝ] (f : F) (r : ℝ) : f r = r