English
A detailed induction-on-r formula expresses ((ofModule M).asAlgebraHom r) m via RestrictScalars and addEquiv.
Русский
Подробная формула по индукции по r выражает ((ofModule M).asAlgebraHom r) m через RestrictScalars и addEquiv.
LaTeX
$$ofModule_asAlgebraHom_apply_apply : ((ofModule M).asAlgebraHom r) m = ...$$
Lean4
@[simp]
theorem ofModule_asAlgebraHom_apply_apply (r : MonoidAlgebra k G) (m : RestrictScalars k (MonoidAlgebra k G) M) :
((ofModule M).asAlgebraHom r) m = (RestrictScalars.addEquiv _ _ _).symm (r • RestrictScalars.addEquiv _ _ _ m) :=
by
apply MonoidAlgebra.induction_on r
· intro g
simp only [one_smul, MonoidAlgebra.lift_symm_apply, MonoidAlgebra.of_apply, Representation.asAlgebraHom_single,
Representation.ofModule, RestrictScalars.lsmul_apply_apply]
· intro f g fw gw
simp only [fw, gw, map_add, add_smul, LinearMap.add_apply]
· intro r f w
simp only [w, map_smul, LinearMap.smul_apply, RestrictScalars.addEquiv_symm_map_smul_smul]
