addHom_ext' — Mathlib

English

For f,g : R[X] →+ M, if ∀ n, f ∘ monomial n = g ∘ monomial n, then f = g.

Русский

Для f,g : R[X] →+ M, если ∀ n, f ∘ monomial n = g ∘ monomial n, то f = g.

LaTeX

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

Lean4

@[ext high]
theorem addHom_ext' {M : Type*} [AddZeroClass M] {f g : R[X] →+ M}
    (h : ∀ n, f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom) : f = g :=
  addHom_ext fun n => DFunLike.congr_fun (h n)

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