Theorem RingHom.IsIntegralElem.of_neg

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.of_negView on Github →