Commit 2024-07-17 14:16 cac1f0d8

View on Github →

feat(FieldTheory/*): prove coprimality of polynomials in terms of roots (#14659)

Estimated changes

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

added theorem Polynomial.aeval_ne_zero_of_isCoprime

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

added theorem Polynomial.isCoprime_iff_aeval_ne_zero