[Merged by Bors] - feat(*): small additions that prepare for Chevalley-Warning

src/algebra/big_operators.lean

@@ -622,10 +622,12 @@ lemma sum_flip [add_comm_monoid β] {n : ℕ} (f : ℕ → β) :
 @prod_flip (multiplicative β) _ _ _
 attribute [to_additive] prod_flip
 
+@[norm_cast]
 lemma sum_nat_cast [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) :
   ↑(s.sum f) = s.sum (λa, f a : α → β) :=
 (nat.cast_add_monoid_hom β).map_sum f s
 
+@[norm_cast]
 lemma prod_nat_cast [comm_semiring β] (s : finset α) (f : α → ℕ) :
   ↑(s.prod f) = s.prod (λa, f a : α → β) :=
 (nat.cast_ring_hom β).map_prod f s
@@ -782,6 +784,11 @@ 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 }
+
 open_locale classical
 
 /-- The product of `f a + g a` over all of `s` is the sum

src/algebra/group_with_zero.lean

@@ -182,6 +182,9 @@ units.ext rfl
   units.mk0 a ha = units.mk0 b hb ↔ a = b :=
 ⟨λ h, by injection h, λ h, units.ext h⟩
 
+@[simp] lemma exists_iff_ne_zero (x : G₀) : (∃ u : units G₀, ↑u = x) ↔ x ≠ 0 :=
+⟨λ ⟨u, hu⟩, by { rw ← hu, exact unit_ne_zero u }, assume hx, ⟨mk0 x hx, rfl⟩⟩
+
 end units
 
 section group_with_zero

src/data/fintype/basic.lean

@@ -575,6 +575,10 @@ finset.card_powerset finset.univ
 instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
 set_fintype _
 
+@[simp] lemma set.to_finset_univ [fintype α] :
+  (set.univ : set α).to_finset = finset.univ :=
+by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
+
 theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] :
   fintype.card {x // p x} ≤ fintype.card α :=
 by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)

src/data/fintype/card.lean

@@ -26,6 +26,22 @@ namespace fintype
 lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
 finset.card_eq_sum_ones _
 
+section
+open finset
+
+variables {ι : Type*} [fintype ι] [decidable_eq ι]
+
+@[to_additive]
+lemma prod_extend_by_one [comm_monoid α] (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
 
 open finset

src/group_theory/order_of_element.lean

@@ -249,6 +249,10 @@ dvd_antisymm
         (by rwa [nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc,
             nat.div_mul_cancel (gcd_dvd_right _ _), mul_comm])))
 
+lemma image_range_order_of (a : α) :
+  finset.image (λ i, a ^ i) (finset.range (order_of a)) = (gpowers a).to_finset :=
+by { ext x, rw [set.mem_to_finset, mem_gpowers_iff_mem_range_order_of] }
+
 omit dec
 open_locale classical
 
@@ -368,6 +372,23 @@ calc (univ.filter (λ a : α, a ^ n = 1)).card ≤ (gpowers (g ^ (fintype.card 
     exact le_of_dvd hn0 (gcd_dvd_left _ _)
   end
 
+section
+
+variables [group α] [fintype α] [decidable_eq α]
+
+lemma is_cyclic.image_range_order_of (ha : ∀ x : α, x ∈ gpowers a) :
+  finset.image (λ i, a ^ i) (range (order_of a)) = univ :=
+begin
+  simp only [image_range_order_of, set.eq_univ_iff_forall.mpr ha],
+  convert set.to_finset_univ
+end
+
+lemma is_cyclic.image_range_card (ha : ∀ x : α, x ∈ gpowers a) :
+  finset.image (λ i, a ^ i) (range (fintype.card α)) = univ :=
+by rw [← order_of_eq_card_of_forall_mem_gpowers ha, is_cyclic.image_range_order_of ha]
+
+end
+
 section totient
 
 variables [group α] [fintype α] [decidable_eq α] (hn : ∀ n : ℕ, 0 < n → (univ.filter (λ a : α, a ^ n = 1)).card ≤ n)