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₂) : M →ₗ[ℚ] M₂

Reinterpret an additive homomorphism as a ℚ-linear map.

Equations

• f.toRatLinearMap = { toFun := (↑f).toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] : Function.Injective 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