Commit 2023-08-27 14:55 1e89b24f

View on Github →

feat: Function.End.one_def and mul_def (#6802)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added theorem Function.End.mul_def

added theorem Function.End.one_def