mathlib

925d8909 - chore(algebra/group/ulift): add missing lemmas about pow, additivize (#15469)

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.