Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.perm.smul_def

Modification history

2021-08-23 14:22
src/group_theory/group_action/group.lean
feat(group_theory/group_action): generalize mul_action.function_End to other endomorphisms (#8724) …
Deleted equiv.perm.smul_defView on Github →
2021-07-22 12:14
src/group_theory/group_action/group.lean
feat(group_theory/group_action): a monoid action determines a monoid hom (#8253) …
Added equiv.perm.smul_defView on Github →