Theorem RatFunc.isAlgebraic_adjoin_simple_X

Modification history

2026-04-05 03:22
Mathlib/FieldTheory/RatFunc/IntermediateField.lean
chore(RatFunc/Luroth): split file and small changes (#37397) …
Modified RatFunc.isAlgebraic_adjoin_simple_XView on Github →
2026-03-05 14:15
Mathlib/FieldTheory/RatFunc/Luroth.lean
feat(RatFunc): add notation for RatFunc (#36172) …
Modified RatFunc.isAlgebraic_adjoin_simple_XView on Github →
2026-03-04 08:58
Mathlib/FieldTheory/RatFunc/Luroth.lean
feat(FieldTheory/RatFunc): Degree of field extension K(X)/K(f) (#34215) …
Added RatFunc.isAlgebraic_adjoin_simple_XView on Github →