Commit 2023-06-23 10:52 995c98a7

View on Github →

feat: add Function.Injective.smulCommClass and Function.Surjective.smulCommClass (#5377)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added theorem Function.Injective.smulCommClass

added theorem Function.Surjective.smulCommClass