coe_toRatLinearMap — Mathlib

English

For a group homomorphism f: M → M₂, the underlying function of the associated ℚ-linear map f.toRatLinearMap is exactly f.

Русский

Для гомоморфизма f: M → M₂ соответствующее ℚ-линейное отображение f.toRatLinearMap имеет тот же функционал, что и f.

LaTeX

$$$\\forall f:\\ M \\to_+ M_2,\\ (\\text{toRatLinearMap}(f)) = f$ as functions.$$

Lean4

@[simp]
theorem coe_toRatLinearMap [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) :
    ⇑f.toRatLinearMap = f :=
  rfl

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