toIntLinearMap_injective — Mathlib

English

The map toIntLinearMap is injective on AddCommGroup homomorphisms.

Русский

Отображение toIntLinearMap инъективно на гомоморфизмах AddCommGroup.

LaTeX

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

Lean4

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

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