subsingleton_id — Mathlib

English

There is essentially only one algebra homomorphism from R to A; i.e., AlgHom_R(R,A) is a subsingleton.

Русский

Существует лишь один алгебраический гомоморфизм от R к A; множество AlgHom_R(R,A) является одиничным (одиночным).

LaTeX

$$$ \\text{Subsingleton}(\\mathrm{AlgHom}_R(R,A)) $$$

Lean4

/-- This is a special case of a more general instance that we define in a later file. -/
instance subsingleton_id : Subsingleton (R →ₐ[R] A) :=
  ⟨fun f g => AlgHom.ext fun _ => (f.commutes _).trans (g.commutes _).symm⟩

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