Theorem RatFunc.natDegree_minpolyX

Modification history

2026-03-04 08:58

Mathlib/FieldTheory/RatFunc/Luroth.lean

feat(FieldTheory/RatFunc): Degree of field extension K(X)/K(f) (#34215) …

Added RatFunc.natDegree_minpolyX View on Github →