Documentation

Mathlib.Algebra.Module.LinearMap.Rat

Reinterpret an additive homomorphism as a -linear map. #

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

Reinterpret an additive homomorphism as a -linear map.

Equations
  • f.toRatLinearMap = { toFun := (↑f).toFun, map_add' := , map_smul' := }
Instances For
    theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [Module M] [AddCommGroup M₂] [Module M₂] :
    Function.Injective AddMonoidHom.toRatLinearMap
    @[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