If u is transcendental over a subfield F of ℂ and uū ∈ F, then a + bu + cū is transcendental over F for all a, b, c ∈ F with (b, c) ≠ (0, 0)
ProvedDiazModulus.transcendental_add_mul_add_mul_conjdiaz-modulus-leannumber-theorytranscendence
Let be a subfield of and transcendental over with . Let with or . Then is transcendental over .
Proof. Put and , which is non-zero as . Multiplying by gives , so is a root of , a polynomial over the intermediate field that is non-zero because or . If were algebraic over , then would be algebraic over , and , algebraic over , would be algebraic over , a contradiction.
Novelty. A standard fact of field theory; routine.
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem transcendental_add_mul_add_mul_conj
(F : Subfield ℂ) (u : ℂ) (hu : Transcendental F u) (hρ : u * conj u ∈ F)
(a b c : ℂ) (ha : a ∈ F) (hb : b ∈ F) (hc : c ∈ F) (hbc : b ≠ 0 ∨ c ≠ 0) :
Transcendental F (a + b * u + c * conj u) := by
sorry
end DiazModulus
Source
Standard field theory. R19 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 18 October 2026 (C. Perassi).