toNatLinearMap_injective — Mathlib

English

The map toNatLinearMap is injective on AddCommMonoid homomorphisms.

Русский

Отображение toNatLinearMap инъективно на множествах гомоморфизмов аддитивных моноидов.

LaTeX

$$Injective toNatLinearMap: ∀ f g, toNatLinearMap f = toNatLinearMap g ⇒ f = g$$

Lean4

theorem toNatLinearMap_injective [AddCommMonoid M] [AddCommMonoid M₂] :
    Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _) :=
  by
  intro f g h
  ext x
  exact LinearMap.congr_fun h x

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