Commit 2023-12-25 13:26 490c92f8

View on Github →

feat(FieldTheory/Separable): add some results regarding separable and no repeated roots (#9263)

  • nodup_[a]roots_iff_of_splits: a polynomial has no repeated roots if and only if it is separable.
  • card_rootSet_eq_natDegree_iff_of_splits: a polynomial has number of roots equal to its degree if and only if it is separable. A converse to card_rootSet_eq_natDegree. Also add some convenience lemmas:
  • Separable.ne_zero: a separable polynomial is not zero.
  • Separable.map_minpoly: if an element is separable over a small field, then it's also separable over a large field.

Estimated changes