Theorem Polynomial.isCoprime_iff_aeval_ne_zero

Modification history

2024-07-17 14:16
Mathlib/FieldTheory/SplittingField/Construction.lean
feat(FieldTheory/*): prove coprimality of polynomials in terms of roots (#14659)
Added Polynomial.isCoprime_iff_aeval_ne_zeroView on Github →