feat(RingTheory): results on resultant (#30983)

Also changed the definition of `sylvesterMatrix` because the old definition has the wrong sign.

Co-authored-by: Oliver Nash <github@olivernash.org>

Author: erdOne

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -356,6 +356,11 @@ theorem prod_eq_single {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈
     (prod_congr rfl fun b hb => h₀ b hb <| by rintro rfl; exact this hb).trans <|
       prod_const_one.trans (h₁ this).symm
 
+@[to_additive (attr := simp)]
+lemma prod_ite_mem_eq [Fintype ι] (s : Finset ι) (f : ι → M) [DecidablePred (· ∈ s)] :
+    (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by
+  rw [← Finset.prod_filter]; congr; aesop
+
 @[to_additive]
 lemma prod_eq_ite [DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι)
     (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) :
@@ -487,7 +492,8 @@ theorem prod_extend_by_one [DecidableEq ι] (s : Finset ι) (f : ι → M) :
     ∏ i ∈ s, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i :=
   (prod_congr rfl) fun _i hi => if_pos hi
 
-@[to_additive]
+/-- Also see `Finset.prod_ite_mem_eq` -/
+@[to_additive /-- Also see `Finset.sum_ite_mem_eq` -/]
 theorem prod_eq_prod_extend (f : s → M) : ∏ x, f x = ∏ x ∈ s, Subtype.val.extend f 1 x := by
   rw [univ_eq_attach, ← Finset.prod_attach s]
   congr with ⟨x, hx⟩

Mathlib/Data/Multiset/Bind.lean

@@ -290,12 +290,21 @@ theorem card_product : card (s ×ˢ t) = card s * card t := by simp [SProd.sprod
 
 variable {s t}
 
-@[simp] lemma mem_product : ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t
-  | (a, b) => by simp [product, and_left_comm]
+@[simp] lemma mem_product : ∀ {p : α × β}, p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
+  | (a, b) => by simp [SProd.sprod, product, and_left_comm]
 
 protected theorem Nodup.product : Nodup s → Nodup t → Nodup (s ×ˢ t) :=
   Quotient.inductionOn₂ s t fun l₁ l₂ d₁ d₂ => by simp [List.Nodup.product d₁ d₂]
 
+@[simp] lemma map_swap_product (s : Multiset α) (t : Multiset β) :
+    (s ×ˢ t).map Prod.swap = t ×ˢ s := by
+  induction s using Multiset.induction <;> simp_all
+
+lemma prod_map_product_eq_prod_prod {M : Type*} [CommMonoid M]
+    (s : Multiset α) (t : Multiset β) (f : α × β → M) :
+    ((s ×ˢ t).map f).prod = (s.map fun i ↦ (t.map fun j ↦ f (i, j)).prod).prod := by
+  induction s using Multiset.induction <;> simp_all
+
 end Product
 
 /-! ### Disjoint sum of multisets -/

Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

@@ -252,6 +252,13 @@ For the `simp` version of this lemma, see `det_submatrix_equiv_self`; this one i
 theorem det_reindex_self (e : m ≃ n) (A : Matrix m m R) : det (reindex e e A) = det A :=
   det_submatrix_equiv_self e.symm A
 
+lemma det_reindex (e e' : m ≃ n) (M : Matrix m m R) :
+    (M.reindex e e').det = sign (e'.trans e.symm) * M.det := by
+  trans ((M.reindex (e.trans e'.symm) (.refl _)).reindex e' e').det
+  · congr 1; ext; simp
+  · simp_rw [det_reindex_self, reindex_apply, Equiv.refl_symm, Equiv.coe_refl, det_permute]
+    rfl
+
 /-- Reindexing both indices along equivalences preserves the absolute of the determinant.
 
 For the `simp` version of this lemma, see `abs_det_submatrix_equiv_equiv`;