addHom_ext — Mathlib

English

Let M be an AddZeroClass. If two additive monoid homomorphisms f,g: R[X] →+ M agree on all monomial generators, then f = g.

Русский

Пусть M — AddZeroClass. Если два гомоморфа f,g: R[X] →+ M совпадают на всех мономиальных порождающих, то f = g.

LaTeX

$$$\forall f,g : R[X] \to_+ M,\; \big(\forall n,a, f(\operatorname{monomial}(n,a)) = g(\operatorname{monomial}(n,a))\big) \Rightarrow f=g$$$

Lean4

theorem addHom_ext {M : Type*} [AddZeroClass M] {f g : R[X] →+ M} (h : ∀ n a, f (monomial n a) = g (monomial n a)) :
    f = g :=
  AddMonoidHom.eq_of_eqOn_denseM addSubmonoid_closure_setOf_eq_monomial <|
    by
    rintro p ⟨n, a, rfl⟩
    exact h n a

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