Commit 2026-02-27 06:57 edb32313

View on Github →

feat: generalize prod_eq_mul_prod_diff_singleton (#35482) Inspired by what prod_eq_single is to prod_eq_single_of_mem, this PR replicates the same idea to prod_eq_mul_prod_diff_singleton.

Estimated changes

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

modified theorem Finset.prod_eq_mul_prod_diff_singleton

added theorem Finset.prod_eq_mul_prod_diff_singleton_of_mem

Modified Mathlib/Algebra/BigOperators/Ring/Finset.lean

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/NoetherNormalization.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/RingTheory/WittVector/TeichmullerSeries.lean