Commit 2026-03-18 16:39 db0e46b8

View on Github →

feat(Adjoin/Polynomial/Bivariate): IsAlgebraic.adjoin_singleton (#35874) This PR builds up to the following theorem:

  • IsAlgebraic.adjoin_singleton: Given two transcendental elements a, b over R, if one of them, say a, is algebraic over R[b] then b is algebraic over R[a]. In particular, it uses maps between R[a] and R[X] as well of some of the Bivariate polynomial API. The results are necessary in preparation for the following: Given a function field K and (y : K) such that (hy : Transcendental Fq y) then we have:
FiniteDimensional Fq⟮y⟯ K

Estimated changes