Theorem minpoly.neg

Modification history

2025-03-17 19:45

Mathlib/FieldTheory/Minpoly/Field.lean

feat: generalize CommRing to Ring/Semiring (#22566) …

Modified minpoly.neg View on Github →

2024-10-07 20:10

Mathlib/FieldTheory/Minpoly/Field.lean

feat(FieldTheory/Minpoly): add theorem for minpoly of -x (#17367) …

Added minpoly.neg View on Github →