{erase_lead, root_isolation}): Add rec_on_erase_lead
#14949

Open

feat(data/polynomial/{erase_lead, root_isolation}): Add rec_on_erase_lead #14949

BoltonBailey wants to merge 5 commits into master from BoltonBailey/rec-on-erase-lead

commit work

dd934a73

complete theorem

6682df6f

golf

a1174e88

move filter singleton

a1ea2ae4

move things

4963b137

mathlib-dependent-issues-bot added blocked-by-other-PR

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR too-late

Milestone

No milestone