If t is transcendental over R and t, z are not algebraically independent over R, then z is algebraic over R[t]

Proved

Transcendence.isAlgebraic_adjoin_of_not_algebraicIndependent_pair

by carlok · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Let $R$ be a commutative ring, $A$ a commutative $R$ -algebra and $t \in A$ transcendental over $R$ . If $t$ and $z \in A$ are not algebraically independent over $R$ , then $z$ is algebraic over the subalgebra $R[t]$ generated by $t$ .

The pair $(t, z)$ is algebraically independent exactly when $t$ is transcendental over $R$ and $z$ is transcendental over $R[t]$ (Mathlib's AlgebraicIndependent.option_iff_transcendental). Over a field, together with Transcendence.trdeg_adjoin_le_one_of_isAlgebraic_adjoin, this shows that elements of which no two are algebraically independent, one of them transcendental, generate an algebra of transcendence degree at most one. DiazModulus.two_algebraically_independent_of_exp_column and DiazModulus.algebraicIndependent_e_pi_of_exp_pi_sq_algebraic use it in this way.

Preamble

import Mathlib

Formal statement

namespace Transcendence

/-- Pair dependence. Let `t` be transcendental over `R`. If the pair `t, z` is not algebraically
independent over `R`, then `z` is algebraic over `R[t]`.

Indeed `t` alone is algebraically independent, and a pair `t, z` with `z` transcendental over
`R[t]` is algebraically independent. Together with
`Transcendence.trdeg_adjoin_le_one_of_isAlgebraic_adjoin`, this turns "no two of these numbers are
algebraically independent, and one of them is transcendental" into "they generate an algebra of
transcendence degree at most one". -/
theorem isAlgebraic_adjoin_of_not_algebraicIndependent_pair {R A : Type*} [CommRing R]
    [CommRing A] [Algebra R A] {t z : A} (ht : Transcendental R t)
    (h : ¬ AlgebraicIndependent R ![t, z]) :
    IsAlgebraic ↥(Algebra.adjoin R ({t} : Set A)) z := by
  sorry

end Transcendence

Source

Standard. Formal proof: Diaz modulus mission, 30 September 2026 (C. Perassi).

View graph