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

Commits
  • WIP
    alreadydone committed 4 years ago
  • Vieta's formula in terms of `polynomial.roots`
    alreadydone committed 4 years ago
  • typo, long line
    alreadydone committed 4 years ago
  • one more dot notation
    alreadydone committed 4 years ago
  • unnecessary `polynomial.` prefixes
    alreadydone committed 4 years ago
  • extraneous instance found by linter
    alreadydone committed 4 years ago
  • make `enum_of_fin_card` take an ordering as args
    alreadydone committed 4 years ago
  • most of the refactor
    hrmacbeth committed 4 years ago
  • sorry-free
    hrmacbeth committed 4 years ago
  • Merge remote-tracking branch 'origin/vieta_multiset' into cubic-discr
    hrmacbeth committed 4 years ago
  • clean up
    hrmacbeth committed 4 years ago
  • lint, upgrade to linear
    hrmacbeth committed 4 years ago
Loading