[Merged by Bors] - feat(field_theory/finite): Chevalley–Warning

src/algebra/big_operators.lean

@@ -504,6 +504,21 @@ begin
     { simp only [mem_image], rintro ⟨⟨_, hm⟩, _, rfl⟩, exact ha hm } }
 end
 
+lemma sum_mul_sum {ι₁ : Type*} {ι₂ : Type*} (s₁ : finset ι₁) (s₂ : finset ι₂)
+  (f₁ : ι₁ → β) (f₂ : ι₂ → β) :
+  s₁.sum f₁ * s₂.sum f₂ = (s₁.product s₂).sum (λ p, f₁ p.1 * f₂ p.2) :=
+by { rw [sum_product, sum_mul, sum_congr rfl], intros, rw mul_sum }
+
+@[move_cast]
+lemma nat_cast_prod (f : α → ℕ) :
+  ((s.prod f : ℕ) : β) = s.prod (λ i, (f i : β)) :=
+(finset.prod_hom _).symm
+
+@[move_cast]
+lemma nat_cast_sum (f : α → ℕ) :
+  ((s.sum f : ℕ) : β) = s.sum (λ i, (f i : β)) :=
+(finset.sum_hom _).symm
+
 end comm_semiring
 
 section integral_domain /- add integral_semi_domain to support nat and ennreal -/

src/data/fintype.lean

@@ -179,6 +179,20 @@ def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
 finset.card_eq_sum_ones _
 
+section
+open_locale classical
+
+@[to_additive]
+lemma prod_extend_by_one [comm_monoid α] {ι} [fintype ι] (s : finset ι) (f : ι → α) :
+  univ.prod (λ i, if i ∈ s then f i else 1) = s.prod f :=
+begin
+  rw [← prod_sdiff (subset_univ s), prod_eq_one, one_mul, prod_congr rfl],
+  { intros i hi, exact dif_pos hi },
+  { intros i hi, rw mem_sdiff at hi, exact dif_neg hi.2 }
+end
+
+end
+
 end fintype
 
 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=

src/data/mv_polynomial.lean

@@ -380,6 +380,8 @@ def eval (f : σ → α) : mv_polynomial σ α → α := eval₂ id f
 
 @[simp] lemma eval_zero : (0 : mv_polynomial σ α).eval f = 0 := eval₂_zero _ _
 
+@[simp] lemma eval_one : (1 : mv_polynomial σ α).eval f = 1 := eval₂_one _ _
+
 @[simp] lemma eval_add : (p + q).eval f = p.eval f + q.eval f := eval₂_add _ _
 
 lemma eval_monomial : (monomial s a).eval f = a * s.prod (λn e, f n ^ e) :=
@@ -391,6 +393,8 @@ eval₂_monomial _ _
 
 @[simp] lemma eval_mul : (p * q).eval f = p.eval f * q.eval f := eval₂_mul _ _
 
+@[simp] lemma eval_pow (n:ℕ) : (p^n).eval f = (p.eval f)^n := eval₂_pow _ _
+
 instance eval.is_semiring_hom : is_semiring_hom (eval f) :=
 eval₂.is_semiring_hom _ _
 
@@ -621,7 +625,7 @@ begin
   exact finset.sup_le (assume s hs, multiset.card_le_of_le $ finset.le_sup hs)
 end
 
-lemma total_degree_C (a : α) : (C a : mv_polynomial σ α).total_degree = 0 :=
+@[simp] lemma total_degree_C (a : α) : (C a : mv_polynomial σ α).total_degree = 0 :=
 nat.eq_zero_of_le_zero $ finset.sup_le $ assume n hn,
   have _ := finsupp.support_single_subset hn,
   begin
@@ -630,12 +634,20 @@ nat.eq_zero_of_le_zero $ finset.sup_le $ assume n hn,
     exact le_refl _
   end
 
-lemma total_degree_zero : (0 : mv_polynomial σ α).total_degree = 0 :=
+@[simp] lemma total_degree_zero : (0 : mv_polynomial σ α).total_degree = 0 :=
 by rw [← C_0]; exact total_degree_C (0 : α)
 
-lemma total_degree_one : (1 : mv_polynomial σ α).total_degree = 0 :=
+@[simp] lemma total_degree_one : (1 : mv_polynomial σ α).total_degree = 0 :=
 total_degree_C (1 : α)
 
+@[simp] lemma total_degree_X {α} [nonzero_comm_ring α] (s : σ) :
+  (X s : mv_polynomial σ α).total_degree = 1 :=
+begin
+  rw [total_degree, X, monomial, finsupp.support_single_ne_zero one_ne_zero],
+  simp only [finset.sup, sum_single_index, finset.insert_empty_eq_singleton,
+    finset.fold_singleton, lattice.sup_bot_eq],
+end
+
 lemma total_degree_add (a b : mv_polynomial σ α) :
   (a + b).total_degree ≤ max a.total_degree b.total_degree :=
 finset.sup_le $ assume n hn,
@@ -660,6 +672,17 @@ finset.sup_le $ assume n hn,
     { assume a b₁ b₂, refl }
   end
 
+lemma total_degree_pow (a : mv_polynomial σ α) (n : ℕ) :
+  (a^n).total_degree ≤ n * a.total_degree :=
+begin
+  induction n with n ih,
+  { simp only [nat.nat_zero_eq_zero, zero_mul, pow_zero, total_degree_one] },
+  rw pow_succ,
+  calc total_degree (a * a ^ n) ≤ a.total_degree + (a^n).total_degree : total_degree_mul _ _
+    ... ≤ a.total_degree + n * a.total_degree : add_le_add_left ih _
+    ... = (n+1) * a.total_degree : by rw [add_mul, one_mul, add_comm]
+end
+
 lemma total_degree_list_prod :
   ∀(s : list (mv_polynomial σ α)), s.prod.total_degree ≤ (s.map mv_polynomial.total_degree).sum
 | []        := by rw [@list.prod_nil (mv_polynomial σ α) _, total_degree_one]; refl
@@ -811,6 +834,20 @@ lemma map_sub : (p - q).map f = p.map f - q.map f := is_ring_hom.map_sub _
 
 end map
 
+section total_degree
+
+@[simp] lemma total_degree_neg (a : mv_polynomial σ α) :
+  (-a).total_degree = a.total_degree :=
+by simp only [total_degree, finsupp.support_neg]
+
+lemma total_degree_sub (a b : mv_polynomial σ α) :
+  (a - b).total_degree ≤ max a.total_degree b.total_degree :=
+calc (a - b).total_degree = (a + -b).total_degree                : by rw sub_eq_add_neg
+                      ... ≤ max a.total_degree (-b).total_degree : total_degree_add a (-b)
+                      ... = max a.total_degree b.total_degree    : by rw total_degree_neg
+
+end total_degree
+
 end comm_ring
 
 section rename