[Merged by Bors] - feat(data/polynomial): Add Partial Fraction Decomposition (Existence)#17709
[Merged by Bors] - feat(data/polynomial): Add Partial Fraction Decomposition (Existence)#17709thefundamentaltheor3m wants to merge 65 commits intomasterfrom
Conversation
| If f, g₁, g₂, ..., gₙ ∈ R[X] and the gᵢs are all monic and pairwise coprime, then ∃ q, r₁, ..., rₙ | ||
| ∈ R[X] such that f / g₁g₂...gₙ = q + r₁/g₁ + ... + rₙ/gₙ and for all i, deg(rᵢ) < deg(gᵢ).#check | ||
|
|
||
| * The result is formalized here in slightly more generality, using finsets. |
There was a problem hiding this comment.
This comment is very hard to read without looking at the actual statement.
By the way, you should call out the main statement in this module docstring. Right now the file is very short but it will be harder to find after you'll add uniqueness.
There was a problem hiding this comment.
I have revised the comment to include more detail, but I understand what you mean about it being unclear unless you look at the actual statement.
I have added docstrings to both theorems, but I'm not sure what you mean when you say I should call out the main statement in the module docstring...
Vierkantor
left a comment
There was a problem hiding this comment.
This is looking quite good already!
Sorting imports Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Vierkantor
left a comment
There was a problem hiding this comment.
Thank you for the PR! Let's get it merged, and I'll let you decide in which form.
bors d+
|
✌️ thefundamentaltheor3m can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…#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>
|
Pull request successfully merged into master. Build succeeded: |
Formalisation and proof of the existence of Partial Fraction Decomposition over an integral domain.