Commit 2025-11-20 10:49 f7c46cf8

View on Github →

feat(RingTheory): results on resultant (#30983) Also changed the definition of sylvesterMatrix because the old definition has the wrong sign.

Estimated changes

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

added theorem Finset.prod_ite_mem_eq

Modified Mathlib/Data/Multiset/Bind.lean

added theorem Multiset.map_swap_product

modified theorem Multiset.mem_product

added theorem Multiset.prod_map_product_eq_prod_prod

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

added theorem Matrix.det_reindex

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

added theorem Polynomial.resultant_C_left

added theorem Polynomial.resultant_C_mul_left

added theorem Polynomial.resultant_C_mul_right

modified theorem Polynomial.resultant_C_right

added theorem Polynomial.resultant_C_zero_left

modified theorem Polynomial.resultant_C_zero_right

added theorem Polynomial.resultant_X_sub_C_left

added theorem Polynomial.resultant_X_sub_C_right

added theorem Polynomial.resultant_add_left_deg

added theorem Polynomial.resultant_add_mul_left

added theorem Polynomial.resultant_add_mul_right

added theorem Polynomial.resultant_add_right_deg

added theorem Polynomial.resultant_comm

added theorem Polynomial.resultant_eq_zero_of_lt_lt

added theorem Polynomial.resultant_map_map

added theorem Polynomial.resultant_one_left

added theorem Polynomial.resultant_one_right

added theorem Polynomial.resultant_succ_left_deg

added theorem Polynomial.resultant_zero_left

added theorem Polynomial.resultant_zero_left_deg

added theorem Polynomial.resultant_zero_right

added theorem Polynomial.resultant_zero_right_deg

added theorem Polynomial.resultant_zero_zero

modified def Polynomial.sylvester

deleted theorem Polynomial.sylvester_C_right

added theorem Polynomial.sylvester_comm

added theorem Polynomial.sylvester_map_map

added theorem Polynomial.sylvester_zero_left_deg

Modified Mathlib/RingTheory/WittVector/MulCoeff.lean