Def MulSemiringAction.compHom
Modification history
2024-05-07 01:05
Mathlib/Algebra/GroupRingAction/Basic.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted MulSemiringAction.compHomView on Github →2022-12-26 20:25
Mathlib/Algebra/GroupRingAction/Basic.lean
feat port: Algebra.GroupRingAction.Basic (#1225) …
Added MulSemiringAction.compHomView on Github →