From 3d0a6ce094e182c8857c3a7157477868a86316c7 Mon Sep 17 00:00:00 2001
From: acmepjz <acme_pjz@hotmail.com>
Date: Wed, 17 Jan 2024 08:00:28 +0800
Subject: [PATCH 1/2] add `sum_pow_{char|expChar}_pow`

---
 Mathlib/Algebra/CharP/Basic.lean   | 21 ++++++++++++++
 Mathlib/Algebra/CharP/ExpChar.lean | 44 ++++++++++++++++++++++++++++++
 2 files changed, 65 insertions(+)

diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index 4bacee9dfbeae..872c9bc3915f6 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -442,6 +442,27 @@ theorem sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) :
   (frobenius R p).map_sum _ _
 #align sum_pow_char sum_pow_char
 
+variable (n : ℕ)
+
+theorem list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum := by
+  induction' n with n ih
+  · simp_rw [pow_zero, pow_one, List.map_id']
+  simp_rw [pow_succ', pow_mul, ih, list_sum_pow_char, List.map_map]
+  rfl
+
+theorem multiset_sum_pow_char_pow (s : Multiset R) :
+    s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum := by
+  induction' n with n ih
+  · simp_rw [pow_zero, pow_one, Multiset.map_id']
+  simp_rw [pow_succ', pow_mul, ih, multiset_sum_pow_char, Multiset.map_map]
+  rfl
+
+theorem sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
+    (∑ i in s, f i) ^ p ^ n = ∑ i in s, f i ^ p ^ n := by
+  induction' n with n ih
+  · simp_rw [pow_zero, pow_one]
+  simp_rw [pow_succ', pow_mul, ih, sum_pow_char]
+
 end CommSemiring
 
 section CommRing
diff --git a/Mathlib/Algebra/CharP/ExpChar.lean b/Mathlib/Algebra/CharP/ExpChar.lean
index 394656137aa7a..b7adc6dd45b9a 100644
--- a/Mathlib/Algebra/CharP/ExpChar.lean
+++ b/Mathlib/Algebra/CharP/ExpChar.lean
@@ -243,3 +243,47 @@ theorem ExpChar.neg_one_pow_expChar_pow [Ring R] (q n : ℕ) [hR : ExpChar R q]
   cases' hR with _ _ hprime _
   · simp only [one_pow, pow_one]
   haveI := Fact.mk hprime; exact CharP.neg_one_pow_char_pow R q n
+
+section BigOperators
+
+open BigOperators
+
+variable {R}
+
+variable [CommSemiring R] (q : ℕ) [hR : ExpChar R q] (n : ℕ)
+
+theorem list_sum_pow_expChar (l : List R) : l.sum ^ q = (l.map (· ^ q : R → R)).sum := by
+  cases' hR with _ _ hprime _
+  · simp_rw [pow_one, List.map_id']
+  haveI := Fact.mk hprime; exact list_sum_pow_char q l
+
+theorem multiset_sum_pow_expChar (s : Multiset R) : s.sum ^ q = (s.map (· ^ q : R → R)).sum := by
+  cases' hR with _ _ hprime _
+  · simp_rw [pow_one, Multiset.map_id']
+  haveI := Fact.mk hprime; exact multiset_sum_pow_char q s
+
+theorem sum_pow_expChar {ι : Type*} (s : Finset ι) (f : ι → R) :
+    (∑ i in s, f i) ^ q = ∑ i in s, f i ^ q := by
+  cases' hR with _ _ hprime _
+  · simp_rw [pow_one]
+  haveI := Fact.mk hprime; exact sum_pow_char q s f
+
+theorem list_sum_pow_expChar_pow (l : List R) :
+    l.sum ^ q ^ n = (l.map (· ^ q ^ n : R → R)).sum := by
+  cases' hR with _ _ hprime _
+  · simp_rw [one_pow, pow_one, List.map_id']
+  haveI := Fact.mk hprime; exact list_sum_pow_char_pow q n l
+
+theorem multiset_sum_pow_expChar_pow (s : Multiset R) :
+    s.sum ^ q ^ n = (s.map (· ^ q ^ n : R → R)).sum := by
+  cases' hR with _ _ hprime _
+  · simp_rw [one_pow, pow_one, Multiset.map_id']
+  haveI := Fact.mk hprime; exact multiset_sum_pow_char_pow q n s
+
+theorem sum_pow_expChar_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
+    (∑ i in s, f i) ^ q ^ n = ∑ i in s, f i ^ q ^ n := by
+  cases' hR with _ _ hprime _
+  · simp_rw [one_pow, pow_one]
+  haveI := Fact.mk hprime; exact sum_pow_char_pow q n s f
+
+end BigOperators

From e61c3670cdde1b70bc28a43d7d63d0562aebf569 Mon Sep 17 00:00:00 2001
From: acmepjz <acme_pjz@hotmail.com>
Date: Thu, 18 Jan 2024 04:21:44 +0800
Subject: [PATCH 2/2] apply suggestions

---
 Mathlib/Algebra/CharP/Basic.lean   | 20 ++++++++---------
 Mathlib/Algebra/CharP/ExpChar.lean | 36 +++++++++++++++---------------
 2 files changed, 27 insertions(+), 29 deletions(-)

diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index 872c9bc3915f6..754a64e259932 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -445,23 +445,21 @@ theorem sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) :
 variable (n : ℕ)
 
 theorem list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum := by
-  induction' n with n ih
-  · simp_rw [pow_zero, pow_one, List.map_id']
-  simp_rw [pow_succ', pow_mul, ih, list_sum_pow_char, List.map_map]
-  rfl
+  induction n
+  case zero => simp_rw [pow_zero, pow_one, List.map_id']
+  case succ n ih => simp_rw [pow_succ', pow_mul, ih, list_sum_pow_char, List.map_map]; rfl
 
 theorem multiset_sum_pow_char_pow (s : Multiset R) :
     s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum := by
-  induction' n with n ih
-  · simp_rw [pow_zero, pow_one, Multiset.map_id']
-  simp_rw [pow_succ', pow_mul, ih, multiset_sum_pow_char, Multiset.map_map]
-  rfl
+  induction n
+  case zero => simp_rw [pow_zero, pow_one, Multiset.map_id']
+  case succ n ih => simp_rw [pow_succ', pow_mul, ih, multiset_sum_pow_char, Multiset.map_map]; rfl
 
 theorem sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ p ^ n = ∑ i in s, f i ^ p ^ n := by
-  induction' n with n ih
-  · simp_rw [pow_zero, pow_one]
-  simp_rw [pow_succ', pow_mul, ih, sum_pow_char]
+  induction n
+  case zero => simp_rw [pow_zero, pow_one]
+  case succ n ih => simp_rw [pow_succ', pow_mul, ih, sum_pow_char]
 
 end CommSemiring
 
diff --git a/Mathlib/Algebra/CharP/ExpChar.lean b/Mathlib/Algebra/CharP/ExpChar.lean
index b7adc6dd45b9a..24ba6bf99c2ad 100644
--- a/Mathlib/Algebra/CharP/ExpChar.lean
+++ b/Mathlib/Algebra/CharP/ExpChar.lean
@@ -253,37 +253,37 @@ variable {R}
 variable [CommSemiring R] (q : ℕ) [hR : ExpChar R q] (n : ℕ)
 
 theorem list_sum_pow_expChar (l : List R) : l.sum ^ q = (l.map (· ^ q : R → R)).sum := by
-  cases' hR with _ _ hprime _
-  · simp_rw [pow_one, List.map_id']
-  haveI := Fact.mk hprime; exact list_sum_pow_char q l
+  cases hR
+  case zero => simp_rw [pow_one, List.map_id']
+  case prime hprime _ => haveI := Fact.mk hprime; exact list_sum_pow_char q l
 
 theorem multiset_sum_pow_expChar (s : Multiset R) : s.sum ^ q = (s.map (· ^ q : R → R)).sum := by
-  cases' hR with _ _ hprime _
-  · simp_rw [pow_one, Multiset.map_id']
-  haveI := Fact.mk hprime; exact multiset_sum_pow_char q s
+  cases hR
+  case zero => simp_rw [pow_one, Multiset.map_id']
+  case prime hprime _ => haveI := Fact.mk hprime; exact multiset_sum_pow_char q s
 
 theorem sum_pow_expChar {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ q = ∑ i in s, f i ^ q := by
-  cases' hR with _ _ hprime _
-  · simp_rw [pow_one]
-  haveI := Fact.mk hprime; exact sum_pow_char q s f
+  cases hR
+  case zero => simp_rw [pow_one]
+  case prime hprime _ => haveI := Fact.mk hprime; exact sum_pow_char q s f
 
 theorem list_sum_pow_expChar_pow (l : List R) :
     l.sum ^ q ^ n = (l.map (· ^ q ^ n : R → R)).sum := by
-  cases' hR with _ _ hprime _
-  · simp_rw [one_pow, pow_one, List.map_id']
-  haveI := Fact.mk hprime; exact list_sum_pow_char_pow q n l
+  cases hR
+  case zero => simp_rw [one_pow, pow_one, List.map_id']
+  case prime hprime _ => haveI := Fact.mk hprime; exact list_sum_pow_char_pow q n l
 
 theorem multiset_sum_pow_expChar_pow (s : Multiset R) :
     s.sum ^ q ^ n = (s.map (· ^ q ^ n : R → R)).sum := by
-  cases' hR with _ _ hprime _
-  · simp_rw [one_pow, pow_one, Multiset.map_id']
-  haveI := Fact.mk hprime; exact multiset_sum_pow_char_pow q n s
+  cases hR
+  case zero => simp_rw [one_pow, pow_one, Multiset.map_id']
+  case prime hprime _ => haveI := Fact.mk hprime; exact multiset_sum_pow_char_pow q n s
 
 theorem sum_pow_expChar_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ q ^ n = ∑ i in s, f i ^ q ^ n := by
-  cases' hR with _ _ hprime _
-  · simp_rw [one_pow, pow_one]
-  haveI := Fact.mk hprime; exact sum_pow_char_pow q n s f
+  cases hR
+  case zero => simp_rw [one_pow, pow_one]
+  case prime hprime _ => haveI := Fact.mk hprime; exact sum_pow_char_pow q n s f
 
 end BigOperators