Commit 2026-03-13 19:39 07642720

View on Github →

feat: uniqueness of partial fraction decomposition (#35702) We prove a uniqueness theorem for each existence theorem in the file.

Estimated changes

Modified Mathlib/Algebra/Polynomial/PartialFractions.lean

modified theorem Polynomial.eq_quo_mul_pow_add_sum_rem_mul_pow

modified theorem Polynomial.eq_quo_mul_prod_add_sum_rem_mul_prod

modified theorem Polynomial.eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow

modified theorem Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse

added theorem Polynomial.quo_add_rem_div_add_rem_div_unique

added theorem Polynomial.quo_add_sum_rem_div_unique

added theorem Polynomial.quo_add_sum_rem_mul_pow_inverse_unique

added theorem Polynomial.quo_mul_pow_add_sum_rem_mul_pow_unique

added theorem Polynomial.quo_mul_prod_add_sum_rem_mul_prod_unique

added theorem Polynomial.quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique