algHom_ext — Mathlib

English

If two algebra homomorphisms from MvPolynomial σ R to A agree on all X_i, they are equal.

Русский

Если два алгебра-гомоморфизма от MvPolynomial σ R в A совпадают на всех X_i, то они равны.

LaTeX

$$$\\\\forall f,g: MvPolynomial\\\\sigma\\\\,R \\\\to_A A, \\\\Big( \\\\forall i, f(X i) = g(X i) \\\\Big) \\\\Rightarrow f = g$$$

Lean4

@[ext 1200]
theorem algHom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : MvPolynomial σ R →ₐ[R] A}
    (hf : ∀ i : σ, f (X i) = g (X i)) : f = g :=
  AddMonoidAlgebra.algHom_ext' (mulHom_ext' fun X : σ => MonoidHom.ext_mnat (hf X))

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