unique — Mathlib

English

There exists no nontrivial ring homomorphism ℝ →+* ℝ; only the identity map exists.

Русский

Не существует ненулевого кольцевого гомоморфизма ℝ →+* ℝ; существует только тождественный отображение.

LaTeX

$$$\forall f:\,\mathbb{R} \to+* \mathbb{R},\ f = \mathrm{id}_{\mathbb{R}}$$$

Lean4

/-- There exists no nontrivial ring homomorphism `ℝ →+* ℝ`. -/
instance unique : Unique (ℝ →+* ℝ) where
  default := RingHom.id ℝ
  uniq
    f :=
    congr_arg OrderRingHom.toRingHom
      (@Subsingleton.elim (ℝ →+*o ℝ) _ ⟨f, ringHom_monotone (fun r hr => ⟨√r, sq_sqrt hr⟩) f⟩ default)

Похожие утверждения