Theorem IsAdjoinRootMonic.minpoly_eq

Modification history

2026-01-13 19:40
Mathlib/RingTheory/IsAdjoinRoot.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified IsAdjoinRootMonic.minpoly_eqView on Github →
2023-06-19 04:18
Mathlib/RingTheory/IsAdjoinRoot.lean
feat: port RingTheory.IsAdjoinRoot (#5190)
Added IsAdjoinRootMonic.minpoly_eqView on Github →