Documentation

Mathlib.Algebra.Module.LinearMap.Rat

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

source
🔸 coverage
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.

Instances For
    source
    📐 coverage
    theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] :
    Function.Injective toRatLinearMap
    source
    📐 coverage
    @[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