Module instances for FunLike types

In this file we define various instances related to modules for FunLike types.

Note that currently, these are not registered as instances, but only abbrevs to avoid long typeclass searches.

@[reducible, inline]

abbrev FunLike.module {M : Type u_1} {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Semiring M] [AddCommMonoid β] [Module M β] [AddCommMonoid F] [IsZeroApply F] [IsAddApply F] [SMul M F] [IsSMulApply M F] : Module M F

A FunLike type is a Module if β is a Module.

Equations

• FunLike.module = Function.Injective.module M (FunLike.coeAddMonoidHom F α β) ⋯ ⋯

theorem FunLike.moduleIsTorsionFree {M : Type u_1} {F : Type u_2} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Semiring M] [AddCommMonoid β] [Module M β] [AddCommMonoid F] [Module M F] [IsSMulApply M F] [Module.IsTorsionFree M β] : Module.IsTorsionFree M F