toRatLinearMap_injective — Mathlib

English

Let M and M2 be additive commutative groups with a ℚ-vector space structure. The map that sends each additive group homomorphism f: M → M₂ to its associated ℚ-linear map is injective.

Русский

Пусть M и M₂ — коммутативные группы с структурой ℚ-векторного пространства. Отображение, отправляющее любую гомоморфизм как абелевой группы f: M → M₂ в соответствующее ℚ-линейное отображение, инъективно.

LaTeX

$$$\\forall f,g:\\ M \\to_+ M_2,\\ (f_{\\mathbb{Q}} = g_{\\mathbb{Q}}) \\Rightarrow f = g.$$$

Lean4

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

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