mathlib3

6e70e0d4 - feat(data/polynomial): Add Partial Fraction Decomposition (Existence) (#17709)

feat(data/polynomial): Add Partial Fraction Decomposition (Existence) (#17709) Formalisation and proof of the existence of Partial Fraction Decomposition over an integral domain. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Sidharth Hariharan <fundamental.theor3m@gmail.com>