Theorem DomMulAct.coe_smul_addMonoidHom

Modification history

2024-02-27 08:54
Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean
feat(Algebra/Module/LinearMap/Basic): module structures of (semi)-linear maps over `DomMulAct` of a ring (#10766) …
Added DomMulAct.coe_smul_addMonoidHomView on Github →