algHom_subsingleton — Mathlib

English

If f = g, then AdjoinRoot f is canonically isomorphic to AdjoinRoot g via algEquivOfEq.

Русский

Если f = g, то AdjoinRoot f канонически изоморфен AdjoinRoot g через algEquivOfEq.

LaTeX

$$$AdjoinRoot f \\cong_{R} AdjoinRoot g$ при $f = g$$$

Lean4

theorem algHom_subsingleton {S : Type*} [CommRing S] [Algebra R S] {r : R} :
    Subsingleton (AdjoinRoot (C r * X - 1) →ₐ[R] S) :=
  ⟨fun f g =>
    algHom_ext
      (@inv_unique _ _ (algebraMap R S r) _ _ (by rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one])
        (by rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]))⟩

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