Theorem RatFunc.Luroth.Φ_natDegree_eq_φ_natDegree

Modification history

2026-03-06 21:32
Mathlib/FieldTheory/RatFunc/Luroth.lean
feat(FieldTheory/RatFunc): Lüroth's theorem (#36109)
Added RatFunc.Luroth.Φ_natDegree_eq_φ_natDegreeView on Github →