Commit 2026-03-04 08:58 b66958d5
View on Github →feat(FieldTheory/RatFunc): Degree of field extension K(X)/K(f) (#34215) Prove that the degree of the field extension K(X)/K(f) of a rational function f equals the maximum of the degrees of its numerator and denominator. This is a crucial lemma towards proving Luroth's theorem. This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.