mathlib3
feat(data/polynomial/partial_fractions): Uniqueness of Partial Fraction Decomposition
#18235
Open
Open
feat(data/polynomial/partial_fractions): Uniqueness of Partial Fraction Decomposition #18235
thefundamentaltheor3m
wants to merge
82 commits into
master
from
xena-partial-fractions-uniqueness
initial commit with docstring
a86363fa
add first question
f0da3978
add solution to first question
deb3a60e
puzzle for UGs
48fd677f
Proof for 2 Denominators
79e9f297
formatting
895f5b36
Name
07774205
tidy up two denominator case
4552bcc1
add coprimality condition
0e7fb694
switch to finsets
af9fd56e
finite product of monics + progress on main result
63793697
Some cleaning up
87404e48
More cleaning up
20ff6529
Progress and unusual error...
cf04319c
some progress and an unusual error
5f230754
some fixes, annoying norm_cast lemma
971e7da0
Some norm_cast lemmas
4b068874
updates
30a0acea
closing important goal
6a46ecee
Restructuring the Coprimality result
528d35d4
more progress
972bad25
some progress with coprimality
9d94f011
Coprimality Proof
f9972223
cleaning up
c4d5c1cc
Merge branch 'master' into xena-partial-fractions
05c2ed1e
add some norm_cast lemmas, delete an unused lemma
47e7a4b3
remove `sum_eq_of_terms_eq`, it's a special case of `finset.congr_sum`
55e21eee
remove dead code
0c652a2b
golf div_eq_quo_add_sum_rem_div, start on uniqueness
6076dc58
fix authors field
885b46de
Merge branch 'xena-partial-fractions' of github.com:leanprover-commun…
bf79aa6c
change from coercion to lift
bd08a774
reorganise API for `algebra_map.has_lift_t`
e80d301e
Merge branch 'master' into xena-partial-fractions
ba674029
bump mathlib
a536ef73
update coe_inj info
6c68af49
refactor: uniqueness for finsets not fintypes
19723953
fixed up finset version of uniqueness
9fe93f87
edit
ce4fa697
edit
6c3b0c83
Merge branch 'master' into xena-partial-fractions
c074418c
removing the injection lemma for coercion
ecdbba08
cleaning up
44e23739
finishing touches
70790995
import tactic to import tactic.linear_combination
2a1df27e
module docstring
2301a583
Update src/data/polynomial/partial_fractions.lean
ced7e03a
Update src/data/polynomial/partial_fractions.lean
31174404
Incorporating formatting suggestions
52ee80b5
moving div_eq_quo_add_rem_div to ring_theory.integral_domain
80642e84
formatting
cd924335
correcting formatting error in documentation
75e367de
incorporating suggestions
89eba6c5
Fixing an error and adding a docstring
bd6be8d1
Docstring for two denominators
4d37e6b3
Update src/data/polynomial/partial_fractions.lean
a662f7c4
Update src/ring_theory/integral_domain.lean
19d7eac2
Update src/data/polynomial/partial_fractions.lean
a075ab24
Update src/data/polynomial/partial_fractions.lean
1eee4e62
Update src/data/polynomial/partial_fractions.lean
4d3f20ef
Update src/data/polynomial/partial_fractions.lean
da24c475
add exists_quotient_remainder
113af172
Update src/ring_theory/integral_domain.lean
ab2ac66c
copyright
0f8c7d0c
remove exists_quotient_remainder
6ca9b5a8
uniqueness scratch
7c9ece51
more progress
718a54b5
update
97d41ad2
adding a new zero lemma
9bc97244
working on the zero case
122b0531
adding new temporary lemma about zero case
5d95f0a7
comments indicating which lemmas will be removed
2a574b19
more attempts with the zero case
9a76064d
trying to simplify using finset.filter
ddebd313
trying to simplify the fraction
c5e9a490
adding in the example
4c6bcc04
finset.sum_prod_div
5af12c9f
useful lemmas
3d44bf47
adding the much-needed have
f678e03d
inching closer
a7a5a85b
majority of general case
3e94204e
a few changes
75553f03
Reviewers
No reviews
Assignees
No one assigned
Labels
WIP
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub