Theorem Polynomial.disc_C

Modification history

2025-10-20 10:08
Mathlib/RingTheory/Polynomial/Resultant/Basic.lean
chore: change `disc` to `discr` to denote the discriminant (#30709) …
Deleted Polynomial.disc_CView on Github →
2025-09-03 09:57
Mathlib/RingTheory/Polynomial/Resultant/Basic.lean
feat(RingTheory/Polynomial): define discriminant (#29252)
Added Polynomial.disc_CView on Github →