feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow (…

…leanprover-community#9799)
FormalMathematicsLab · Jan 18, 2024 · 1e74fcf · 1e74fcf
1 parent 2a14ea0
commit 1e74fcf
Show file tree

Hide file tree

Showing 2 changed files with 63 additions and 0 deletions.
diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
@@ -442,6 +442,25 @@ 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
+  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
+  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
+  case zero => simp_rw [pow_zero, pow_one]
+  case succ n ih => 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
@@ -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
+  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
+  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
+  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
+  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
+  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
+  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