Documentation

Mathlib.Data.Real.CompleteField

The reals are a conditionally complete linearly ordered field #

source
🔸 coverage
noncomputable instance instConditionallyCompleteLinearOrderedFieldReal :
ConditionallyCompleteLinearOrderedField ℝ

The reals are a conditionally complete linearly ordered field.

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

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

    Equations
      source
      📐 coverage
      @[simp]
      theorem Real.ringHom_apply {F : Type u_1} [FunLike F ℝ ℝ] [RingHomClass F ℝ ℝ] (f : F) (r : ℝ) :
      f r = r