Mathlib v3 is deprecated. Go to Mathlib v4

Theorem power_basis.degree_minpoly

Modification history

2023-01-14 21:04

src/ring_theory/power_basis.lean

feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117) …

Added power_basis.degree_minpoly View on Github →