Theorem RingHom.IsIntegralElem.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 RingHom.IsIntegralElem.neg_iffView on Github →