mathlib3
feat(algebra/cubic_discriminant): remove custom `cubic` structure and replace by API about new `to_poly`
#15088
Open
Overview
Commits
12
Changes
View On GitHub

feat(algebra/cubic_discriminant): remove custom `cubic` structure and replace by API about new `to_poly` #15088

hrmacbeth wants to merge 12 commits into master from cubic-discr
hrmacbeth
alreadydone WIP
378937fa
alreadydone Vieta's formula in terms of `polynomial.roots`
81b01a53
alreadydone typo, long line
4d15dedb
alreadydone one more dot notation
f58dd26a
alreadydone unnecessary `polynomial.` prefixes
cd3fac0a
alreadydone extraneous instance found by linter
6ce5beae
alreadydone make `enum_of_fin_card` take an ordering as args
c7006ab9
hrmacbeth most of the refactor
2596fe67
hrmacbeth sorry-free
0d1ec867
hrmacbeth Merge remote-tracking branch 'origin/vieta_multiset' into cubic-discr
89bd4ffd
hrmacbeth clean up
e9c300f2
hrmacbeth hrmacbeth added RFC
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
hrmacbeth lint, upgrade to linear
61eae7fc
vihdzp
vihdzp commented on 2022-07-01
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
RFC too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum