feat(*): small additions that prepare for Chevalley-Warning (#2560)

A number a small changes that prepare for #1564.

src/algebra/associated.lean

@@ -11,12 +11,6 @@ import data.multiset
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 
-theorem is_unit.mk0 [division_ring α] (x : α) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
-
-theorem is_unit_iff_ne_zero [division_ring α] {x : α} :
-  is_unit x ↔ x ≠ 0 :=
-⟨λ ⟨u, hu⟩, hu.symm ▸ λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3, is_unit.mk0 x⟩
-
 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
  λ h, begin

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

@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import algebra.group.units
+import algebra.group.is_unit
 
 /-!
 # G₀roups with an adjoined zero element
@@ -182,11 +182,19 @@ 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
 variables {G₀ : Type*} [group_with_zero G₀]
 
+lemma is_unit.mk0 (x : G₀) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
+
+lemma is_unit_iff_ne_zero {x : G₀} : is_unit x ↔ x ≠ 0 :=
+⟨λ ⟨u, hu⟩, hu.symm ▸ λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3, is_unit.mk0 x⟩
+
 lemma mul_eq_zero' (a b : G₀) (h : a * b = 0) : a = 0 ∨ b = 0 :=
 begin
   classical, contrapose! h,

src/data/fintype/basic.lean

@@ -39,6 +39,13 @@ theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
 by simp [ext]
 
+@[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
+  univ ∩ s = s := ext' $ λ a, by simp
+
+@[simp] lemma inter_univ [decidable_eq α] (s : finset α) :
+  s ∩ univ = s :=
+by rw [inter_comm, univ_inter]
+
 @[simp] lemma piecewise_univ [∀i : α, decidable (i ∈ (univ : finset α))]
   {δ : α → Sort*} (f g : Πi, δ i) : univ.piecewise f g = f :=
 by { ext i, simp [piecewise] }
@@ -575,6 +582,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,18 @@ 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 :=
+by rw [← prod_filter, filter_mem_eq_inter, univ_inter]
+
+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)