Theorem IsIntegral.neg_iff

Modification history

2024-10-07 20:10
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
feat(FieldTheory/Minpoly): add theorem for minpoly of -x (#17367) …
Added IsIntegral.neg_iffView on Github →