lhom_ext' — Mathlib

English

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

Русский

Для линейных отображений f,g : R[X] →ₗ[R] M, если ∀ n, f ∘ monomial n = g ∘ monomial n, то f = g.

LaTeX

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

Lean4

@[ext high]
theorem lhom_ext' {M : Type*} [AddCommMonoid M] [Module R M] {f g : R[X] →ₗ[R] M}
    (h : ∀ n, f.comp (monomial n) = g.comp (monomial n)) : f = g :=
  LinearMap.toAddMonoidHom_injective <|
    addHom_ext fun n =>
      LinearMap.congr_fun
        (h n)
          -- this has the same content as the subsingleton

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