Theorem Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed

Modification history

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