Commit 2023-06-23 09:36 84481d0e

View on Github →

feat: define a type synonym for right action on the domain of a function (#5368) Based on this discussion on Zulip

Estimated changes

added def DomMulAct.mk
added theorem DomMulAct.mk_inv
added theorem DomMulAct.mk_mul
added theorem DomMulAct.mk_one
added theorem DomMulAct.mk_pow
added theorem DomMulAct.mk_zpow
added theorem DomMulAct.smul_apply
added theorem DomMulAct.symm_mk_inv
added theorem DomMulAct.symm_mk_mul
added theorem DomMulAct.symm_mk_one
added theorem DomMulAct.symm_mk_pow
added theorem DomMulAct.symm_mk_zpow
added def DomMulAct