Commit 2024-02-27 08:54 27710436

View on Github →

feat(Algebra/Module/LinearMap/Basic): module structures of (semi)-linear maps over DomMulAct of a ring (#10766) splitted from #8559 These are written by @alreadydone

Estimated changes

Modified Mathlib/Algebra/Module/Hom.lean

Modified Mathlib/Algebra/Module/LinearMap/Basic.lean

added theorem DomMulAct.coe_smul_linearMap

added theorem DomMulAct.mk_smul_linearMap_apply

added theorem DomMulAct.smul_linearMap_apply

Modified Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

added theorem DomMulAct.coe_smul_addMonoidHom