Commit 2023-04-28 11:10 81e58562

View on Github →

feat: port CategoryTheory.Action (#3657)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Action.lean

added theorem CategoryTheory.ActionCategory.back_coe

added theorem CategoryTheory.ActionCategory.cases'

added theorem CategoryTheory.ActionCategory.coe_back

added def CategoryTheory.ActionCategory.curry

added def CategoryTheory.ActionCategory.endMulEquivSubgroup

added theorem CategoryTheory.ActionCategory.homOfPair.val

added def CategoryTheory.ActionCategory.homOfPair

added theorem CategoryTheory.ActionCategory.hom_as_subtype

added def CategoryTheory.ActionCategory.objEquiv

added def CategoryTheory.ActionCategory.stabilizerIsoEnd

added theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_apply

added theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply

added def CategoryTheory.ActionCategory.uncurry

added def CategoryTheory.ActionCategory.π

added theorem CategoryTheory.ActionCategory.π_map

added theorem CategoryTheory.ActionCategory.π_obj

added def CategoryTheory.ActionCategory

added def CategoryTheory.actionAsFunctor