linearMap_ext — Mathlib

English

A linear map is uniquely determined by its values on all monomials.

Русский

Линейное отображение однозначно определяется его значениями на всех мономах.

LaTeX

$$$\\\\forall M: {M: type*}, [AddCommMonoid M] [Module R M] {f g: MvPolynomial\\\\,R \\\\to_L[R] M}, \\\\Big( \\\\forall s, f \\\\circ \\\\text{monomial } s = g \\\\circ \\\\text{monomial } s \\\\Big) \\\\Rightarrow f = g$$$

Lean4

@[ext]
theorem linearMap_ext {M : Type*} [AddCommMonoid M] [Module R M] {f g : MvPolynomial σ R →ₗ[R] M}
    (h : ∀ s, f ∘ₗ monomial s = g ∘ₗ monomial s) : f = g :=
  Finsupp.lhom_ext' h

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