Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_monoid.End.smul_def

Modification history

2021-08-23 14:22
src/group_theory/group_action/defs.lean
feat(group_theory/group_action): generalize mul_action.function_End to other endomorphisms (#8724) …
Added add_monoid.End.smul_defView on Github →