English
The action of the module-induced representation on an inductive construct yields a concrete formula for ((ofModule M).asAlgebraHom r) m.
Русский
Действие полученного по модулю представления на элементе дает явное выражение для ((ofModule M).asAlgebraHom r) m.
LaTeX
$$ofModule_asAlgebraHom_apply_apply : ((ofModule M).asAlgebraHom r) m = ...$$
Lean4
/-- Build a `Representation` from a `[Module (MonoidAlgebra k G) M]`.
Note that the representation is built on `restrictScalars k (MonoidAlgebra k G) M`,
rather than on `M` itself.
-/
noncomputable def ofModule : Representation k G (RestrictScalars k (MonoidAlgebra k G) M) :=
(MonoidAlgebra.lift k G (RestrictScalars k (MonoidAlgebra k G) M →ₗ[k] RestrictScalars k (MonoidAlgebra k G) M)).symm
(RestrictScalars.lsmul k (MonoidAlgebra k G) M)
