HepLean Documentation

Mathlib.Algebra.Module.LinearMap.Rat

Reinterpret an additive homomorphism as a ℚ-linear map. #

source
def AddMonoidHom.toRatLinearMap {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) :
M →ₗ[ℚ] M₂

Reinterpret an additive homomorphism as a ℚ-linear map.

Equations
  • f.toRatLinearMap = { toFun := (↑f).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
    source
    theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] :
    Function.Injective AddMonoidHom.toRatLinearMap
    source
    @[simp]
    theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) :
    ⇑f.toRatLinearMap = ⇑f