Theorem Polynomial.card_rootSet_eq_natDegree_iff_of_splits

Modification history

2023-12-25 13:26
Mathlib/FieldTheory/Separable.lean
feat(FieldTheory/Separable): add some results regarding separable and no repeated roots (#9263) …
Added Polynomial.card_rootSet_eq_natDegree_iff_of_splitsView on Github →