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.

src/algebra/group/ulift.lean

@@ -20,7 +20,7 @@ We also provide `ulift.mul_equiv : ulift R ≃* R` (and its additive analogue).
 -/
 
 universes u v
-variables {α : Type u} {x y : ulift.{v} α}
+variables {α : Type u} {β : Type*} {x y : ulift.{v} α}
 
 namespace ulift
 
@@ -36,6 +36,16 @@ namespace ulift
 @[to_additive] instance has_inv [has_inv α] : has_inv (ulift α) := ⟨λ f, ⟨f.down⁻¹⟩⟩
 @[simp, to_additive] lemma inv_down [has_inv α] : x⁻¹.down = (x.down)⁻¹ := rfl
 
+@[to_additive]
+instance has_smul [has_smul α β] : has_smul α (ulift β) := ⟨λ n x, up (n • x.down)⟩
+@[simp, to_additive]
+lemma smul_down [has_smul α β] (a : α) (b : ulift.{v} β) : (a • b).down = a • b.down := rfl
+
+@[to_additive has_smul, to_additive_reorder 1]
+instance has_pow [has_pow α β] : has_pow (ulift α) β := ⟨λ x n, up (x.down ^ n)⟩
+@[simp, to_additive smul_down, to_additive_reorder 1]
+lemma pow_down [has_pow α β] (a : ulift.{v} α) (b : β) : (a ^ b).down = a.down ^ b := rfl
+
 /--
 The multiplicative equivalence between `ulift α` and `α`.
 -/
@@ -59,14 +69,6 @@ equiv.ulift.injective.mul_one_class _ rfl $ λ x y, rfl
 instance mul_zero_one_class [mul_zero_one_class α] : mul_zero_one_class (ulift α) :=
 equiv.ulift.injective.mul_zero_one_class _ rfl rfl $ λ x y, rfl
 
-@[to_additive]
-instance has_smul {β : Type*} [has_smul α β] : has_smul α (ulift β) :=
-⟨λ n x, up (n • x.down)⟩
-
-@[to_additive has_smul, to_additive_reorder 1]
-instance has_pow {β : Type*} [has_pow α β] : has_pow (ulift α) β :=
-⟨λ x n, up (x.down ^ n)⟩
-
 @[to_additive]
 instance monoid [monoid α] : monoid (ulift α) :=
 equiv.ulift.injective.monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

src/algebra/module/ulift.lean

@@ -23,16 +23,13 @@ variable {R : Type u}
 variable {M : Type v}
 variable {N : Type w}
 
+@[to_additive]
 instance has_smul_left [has_smul R M] :
   has_smul (ulift R) M :=
 ⟨λ s x, s.down • x⟩
 
-@[simp] lemma smul_down [has_smul R M] (s : ulift R) (x : M) : (s • x) = s.down • x := rfl
-
-@[simp]
-lemma smul_down' [has_smul R M] (s : R) (x : ulift M) :
-  (s • x).down = s • x.down :=
-rfl
+@[simp, to_additive]
+lemma smul_def [has_smul R M] (s : ulift R) (x : M) : s • x = s.down • x := rfl
 
 instance is_scalar_tower [has_smul R M] [has_smul M N] [has_smul R N]
   [is_scalar_tower R M N] : is_scalar_tower (ulift R) M N :=
@@ -50,16 +47,19 @@ instance [has_smul R M] [has_smul Rᵐᵒᵖ M] [is_central_scalar R M] :
   is_central_scalar R (ulift M) :=
 ⟨λ r m, congr_arg up $ op_smul_eq_smul r m.down⟩
 
+@[to_additive]
 instance mul_action [monoid R] [mul_action R M] : mul_action (ulift R) M :=
 { smul := (•),
   mul_smul := λ _ _, mul_smul _ _,
   one_smul := one_smul _ }
 
+@[to_additive]
 instance mul_action' [monoid R] [mul_action R M] :
   mul_action R (ulift M) :=
 { smul := (•),
-  mul_smul := λ r s f, by { cases f, ext, simp [mul_smul], },
-  one_smul := λ f, by { ext, simp [one_smul], } }
+  mul_smul := λ r s ⟨f⟩, ext _ _ $ mul_smul _ _ _,
+  one_smul := λ ⟨f⟩, ext _ _ $ one_smul _ _,
+  ..ulift.has_smul_left }
 
 instance distrib_mul_action [monoid R] [add_monoid M] [distrib_mul_action R M] :
   distrib_mul_action (ulift R) M :=