ringHom_ext — Mathlib

English

If two ring homomorphisms from the multivariate polynomial ring to a semiring A agree on all constants and on the images of the variables X_i, then they are equal.

Русский

Если два кольцевых однородных гомоморфизма от многочленовой кольцевой алгебры к полупрямому полюсу A совпадают на константах и на образах переменных X_i, то они равны между собой.

LaTeX

$$$\\\\forall f,g: MvPolynomial\\\\sigma\\\\,R \\\\to+* A, \\\\Big( \\\\forall r: R, f(C r) = g(C r) \\\\Big) \\\\land \\\\Big( \\\\forall i: \\sigma, f(X i) = g(X i) \\\\Big) \\\\Rightarrow \\\\ f = g $$$

Lean4

theorem ringHom_ext {A : Type*} [Semiring A] {f g : MvPolynomial σ R →+* A} (hC : ∀ r, f (C r) = g (C r))
    (hX : ∀ i, f (X i) = g (X i)) : f = g :=
  by
  refine
    AddMonoidAlgebra.ringHom_ext' ?_
      ?_
        -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): this has high priority, but Lean still chooses `RingHom.ext`, why?
          -- probably because of the type synonym

  · ext x
    exact hC _
  · apply Finsupp.mulHom_ext'; intro x
    apply MonoidHom.ext_mnat
    exact hX _

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