feat(algebra/hom/equiv/basic): Add to_additive to Pi_congr_right …

…lemmas (#17827)

Add `to_additive` attribute to three lemmas about `mul_equiv.Pi_congr_right`.

src/algebra/hom/equiv/basic.lean

@@ -450,16 +450,16 @@ def Pi_congr_right {η : Type*}
   map_mul' := λ x y, funext $ λ j, (es j).map_mul (x j) (y j),
   .. equiv.Pi_congr_right (λ j, (es j).to_equiv) }
 
-@[simp]
+@[simp, to_additive]
 lemma Pi_congr_right_refl {η : Type*} {Ms : η → Type*} [Π j, has_mul (Ms j)] :
   Pi_congr_right (λ j, mul_equiv.refl (Ms j)) = mul_equiv.refl _ := rfl
 
-@[simp]
+@[simp, to_additive]
 lemma Pi_congr_right_symm {η : Type*}
   {Ms Ns : η → Type*} [Π j, has_mul (Ms j)] [Π j, has_mul (Ns j)]
   (es : ∀ j, Ms j ≃* Ns j) : (Pi_congr_right es).symm = (Pi_congr_right $ λ i, (es i).symm) := rfl
 
-@[simp]
+@[simp, to_additive]
 lemma Pi_congr_right_trans {η : Type*}
   {Ms Ns Ps : η → Type*} [Π j, has_mul (Ms j)] [Π j, has_mul (Ns j)]
   [Π j, has_mul (Ps j)]