Commit 2022-07-18 22:20 925d8909
View on Github →chore(algebra/group/ulift): add missing lemmas about pow, additivize (#15469)
This renames ulift.smul_down to ulift.smul_def since there is no mention of down on the LHS, and then unprimes ulift.smul_down' now that the name is available.
It also additivizes the mul_action instances.