feat: to_additive for pow_boole (#6535)

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1721,6 +1721,7 @@ theorem eq_one_of_prod_eq_one {s : Finset α} {f : α → β} {a : α} (hp : ∏
 #align finset.eq_one_of_prod_eq_one Finset.eq_one_of_prod_eq_one
 #align finset.eq_zero_of_sum_eq_zero Finset.eq_zero_of_sum_eq_zero
 
+@[to_additive sum_boole_nsmul]
 theorem prod_pow_boole [DecidableEq α] (s : Finset α) (f : α → β) (a : α) :
     (∏ x in s, f x ^ ite (a = x) 1 0) = ite (a ∈ s) (f a) 1 := by simp
 #align finset.prod_pow_boole Finset.prod_pow_boole

Mathlib/Algebra/GroupPower/Basic.lean

@@ -48,12 +48,12 @@ section Pow
 
 variable [Pow M ℕ]
 
-@[simp]
+@[to_additive (attr := simp) ite_nsmul]
 theorem pow_ite (P : Prop) [Decidable P] (a : M) (b c : ℕ) :
     (a ^ if P then b else c) = if P then a ^ b else a ^ c := by split_ifs <;> rfl
 #align pow_ite pow_ite
 
-@[simp]
+@[to_additive (attr := simp) nsmul_ite]
 theorem ite_pow (P : Prop) [Decidable P] (a b : M) (c : ℕ) :
     (if P then a else b) ^ c = if P then a ^ c else b ^ c := by split_ifs <;> rfl
 #align ite_pow ite_pow
@@ -106,9 +106,11 @@ theorem pow_two (a : M) : a ^ 2 = a * a := by rw [pow_succ, pow_one]
 alias pow_two ← sq
 #align sq sq
 
+@[to_additive three'_nsmul]
 theorem pow_three' (a : M) : a ^ 3 = a * a * a := by rw [pow_succ', pow_two]
 #align pow_three' pow_three'
 
+@[to_additive three_nsmul]
 theorem pow_three (a : M) : a ^ 3 = a * (a * a) := by rw [pow_succ, pow_two]
 #align pow_three pow_three
 
@@ -148,6 +150,7 @@ theorem pow_mul_comm' (a : M) (n : ℕ) : a ^ n * a = a * a ^ n :=
 #align pow_mul_comm' pow_mul_comm'
 #align nsmul_add_comm' nsmul_add_comm'
 
+@[to_additive boole_nsmul]
 theorem pow_boole (P : Prop) [Decidable P] (a : M) :
     (a ^ if P then 1 else 0) = if P then a else 1 := by simp
 #align pow_boole pow_boole