feat(algebra/big_operators/finprod): add div lemmas (#10472)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/big_operators/finprod.lean

@@ -244,6 +244,10 @@ end
   ∏ᶠ x, (f x)⁻¹ = (∏ᶠ x, f x)⁻¹ :=
 ((mul_equiv.inv G).map_finprod f).symm
 
+lemma finprod_inv_distrib₀ {G : Type*} [comm_group_with_zero G] (f : α → G) :
+  ∏ᶠ x, (f x)⁻¹ = (∏ᶠ x, f x)⁻¹ :=
+((mul_equiv.inv₀ G).map_finprod f).symm
+
 end sort
 
 section type
@@ -318,6 +322,15 @@ begin
   exact (h hxs).2 hx
 end
 
+@[to_additive] lemma finprod_cond_ne (f : α → M) (a : α) [decidable_eq α]
+  (hf : finite (mul_support f)) : (∏ᶠ i ≠ a, f i) = ∏ i in hf.to_finset.erase a, f i :=
+begin
+  apply finprod_cond_eq_prod_of_cond_iff,
+  intros x hx,
+  rw [finset.mem_erase, finite.mem_to_finset, mem_mul_support],
+  exact ⟨λ h, and.intro h hx, λ h, h.1⟩
+end
+
 @[to_additive] lemma finprod_mem_eq_prod_of_inter_mul_support_eq (f : α → M) {s : set α}
   {t : finset α} (h : s ∩ mul_support f = t ∩ mul_support f) :
   ∏ᶠ i ∈ s, f i = ∏ i in t, f i :=
@@ -409,12 +422,18 @@ end
 
 /-- If the multiplicative supports of `f` and `g` are finite, then the product of `f i / g i`
 equals the product of `f i` divided by the product over `g i`. -/
-@[to_additive] lemma finprod_div_distrib {M' : Type*} [comm_group M'] {f g : α → M'}
+@[to_additive] lemma finprod_div_distrib {G : Type*} [comm_group G] {f g : α → G}
   (hf : (mul_support f).finite) (hg : (mul_support g).finite) :
   ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i :=
 by simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mul_support_inv g).symm.rec hg),
               finprod_inv_distrib]
 
+lemma finprod_div_distrib₀ {G : Type*} [comm_group_with_zero G] {f g : α → G}
+  (hf : (mul_support f).finite) (hg : (mul_support g).finite) :
+  ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i :=
+by simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mul_support_inv₀ g).symm.rec hg),
+              finprod_inv_distrib₀]
+
 /-- A more general version of `finprod_mem_mul_distrib` that requires `s ∩ mul_support f` and
 `s ∩ mul_support g` instead of `s` to be finite. -/
 @[to_additive] lemma finprod_mem_mul_distrib' (hf : (s ∩ mul_support f).finite)
@@ -476,12 +495,20 @@ g.to_monoid_hom.map_finprod_mem f hs
   (hs : s.finite) : ∏ᶠ x ∈ s, (f x)⁻¹ = (∏ᶠ x ∈ s, f x)⁻¹ :=
 ((mul_equiv.inv G).map_finprod_mem f hs).symm
 
+lemma finprod_mem_inv_distrib₀ {G : Type*} [comm_group_with_zero G] (f : α → G)
+  (hs : s.finite) : ∏ᶠ x ∈ s, (f x)⁻¹ = (∏ᶠ x ∈ s, f x)⁻¹ :=
+((mul_equiv.inv₀ G).map_finprod_mem f hs).symm
+
 /-- Given a finite set `s`, the product of `f i / g i` over `i ∈ s` equals the product of `f i`
 over `i ∈ s` divided by the product of `g i` over `i ∈ s`. -/
-@[to_additive] lemma finprod_mem_div_distrib {M' : Type*} [comm_group M'] (f g : α → M')
+@[to_additive] lemma finprod_mem_div_distrib {G : Type*} [comm_group G] (f g : α → G)
   (hs : s.finite) : ∏ᶠ i ∈ s, f i / g i = (∏ᶠ i ∈ s, f i) / ∏ᶠ i ∈ s, g i :=
 by simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]
 
+lemma finprod_mem_div_distrib₀ {G : Type*} [comm_group_with_zero G] (f g : α → G)
+  (hs : s.finite) : ∏ᶠ i ∈ s, f i / g i = (∏ᶠ i ∈ s, f i) / ∏ᶠ i ∈ s, g i :=
+by simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib₀ g hs]
+
 /-!
 ### `∏ᶠ x ∈ s, f x` and set operations
 -/
@@ -735,6 +762,23 @@ over `a ∈ ⋃₀ t` is the product over `s ∈ t` of the products of `f a` ove
   ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a :=
 by { rw set.sUnion_eq_bUnion, exact finprod_mem_bUnion h ht₀ ht₁ }
 
+@[to_additive] lemma mul_finprod_cond_ne (a : α) (hf : finite (mul_support f)) :
+  f a * (∏ᶠ i ≠ a, f i) = ∏ᶠ i, f i :=
+begin
+  classical,
+  rw [finprod_eq_prod _ hf],
+  have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.to_finset \ {a}),
+  { intros x hx,
+    rw [finset.mem_sdiff, finset.mem_singleton, finite.mem_to_finset, mem_mul_support],
+    exact ⟨λ h, and.intro hx h, λ h, h.2⟩,},
+  rw [finprod_cond_eq_prod_of_cond_iff f h, finset.sdiff_singleton_eq_erase],
+  by_cases ha : a ∈ mul_support f,
+  { apply finset.mul_prod_erase _ _ ((finite.mem_to_finset _ ).mpr ha), },
+  { rw [mem_mul_support, not_not] at ha,
+    rw [ha, one_mul],
+    apply finset.prod_erase _ ha, }
+end
+
 /-- If `s : set α` and `t : set β` are finite sets, then the product over `s` commutes
 with the product over `t`. -/
 @[to_additive] lemma finprod_mem_comm {s : set α} {t : set β}

src/data/equiv/mul_add.lean

@@ -584,10 +584,20 @@ end equiv
 `mul_equiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case. -/
 @[to_additive "When the `add_group` is commutative, `equiv.neg` is an `add_equiv`."]
 def mul_equiv.inv (G : Type*) [comm_group G] : G ≃* G :=
-{ to_fun := has_inv.inv,
-  inv_fun := has_inv.inv,
+{ to_fun   := has_inv.inv,
+  inv_fun  := has_inv.inv,
   map_mul' := mul_inv,
-  ..equiv.inv G}
+  ..equiv.inv G }
+
+/-- When the group with zero is commutative, `equiv.inv₀` is a `mul_equiv`. -/
+@[simps apply] def mul_equiv.inv₀ (G : Type*) [comm_group_with_zero G] : G ≃* G :=
+{ to_fun   := has_inv.inv,
+  inv_fun  := has_inv.inv,
+  map_mul' := λ x y, mul_inv₀,
+  ..equiv.inv₀ G }
+
+@[simp] lemma mul_equiv.inv₀_symm (G : Type*) [comm_group_with_zero G] :
+  (mul_equiv.inv₀ G).symm = mul_equiv.inv₀ G := rfl
 
 section type_tags