algHom_ext — Mathlib

English

Two R-algebra homomorphisms from AdjoinRoot f to the same S-coefficient algebra are equal if they agree on the image of the root of f.

Русский

Два R-алгебро-хомоморфизма от AdjoinRoot f в одно и то же S-алгебраическое кольцо равны, если они согласованы на корне f.

LaTeX

$$@ext theorem algHom_ext (h : g1(root f) = g2(root f)) : g1 = g2$$

Lean4

/-- Two `R`-`AlgHom` from `AdjoinRoot f` to the same `R`-algebra are the same iff
they agree on `root f`. -/
@[ext]
theorem algHom_ext [Semiring S] [Algebra R S] {g₁ g₂ : AdjoinRoot f →ₐ[R] S} (h : g₁ (root f) = g₂ (root f)) :
    g₁ = g₂ :=
  Ideal.Quotient.algHom_ext R <| Polynomial.algHom_ext h

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