Uniqueness of ring homomorphisms to the real numbers

This file contains results about ring homomorphisms to ℝ.

Main results

• Real.nonemptyOrderRingHom: For any archimedean ordered field α, there exists a monotone ring homomorphism α →+*o ℝ.
• Real.RingHom.unique: There exists no nontrivial ring homomorphism ℝ →+* ℝ.

instance Real.nonemptyOrderRingHom (α : Type u_1) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] : Nonempty (α →+*o ℝ)

theorem ringHom_monotone {R : Type u_1} {S : Type u_2} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [Ring S] [LinearOrder S] [IsOrderedAddMonoid S] [PosMulMono S] (hR : ∀ (r : R), 0 ≤ r → IsSquare r) (f : R →+* S) : Monotone ⇑f

@[implicit_reducible]

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