A transcendental number is a root of no non-zero quadratic with algebraic coefficients

Proved

DiazModulus.quadratic_eq_zero_of_not_mem_Qbar

by carlok · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Let $z$ be a complex number that is not algebraic, and let $a, b, c$ be algebraic. If $az^2 + bz + c = 0$ , then $a = b = c = 0$ .

Proof. Otherwise $z$ would be algebraic over the field of algebraic numbers, and therefore algebraic.

Novelty. None: a standard fact. It is the step that makes families such as $(1, \lambda, \lambda^2)$ or $(1, \lambda, 1/\lambda)$ linearly independent over $\overline{\mathbb{Q}}$ for transcendental $\lambda$ , which Diaz (2007) uses without comment.

Preamble

import Definitions.Def_DiazModulus

Formal statement

open Complex ComplexConjugate

namespace DiazModulus

/-- A complex number outside `Q̄` is a root of no non-zero quadratic polynomial with algebraic coefficients. -/
theorem quadratic_eq_zero_of_not_mem_Qbar {z a b c : ℂ} (hz : z ∉ Qbar)
    (ha : a ∈ Qbar) (hb : b ∈ Qbar) (hc : c ∈ Qbar) (h : a * z ^ 2 + b * z + c = 0) :
    a = 0 ∧ b = 0 ∧ c = 0 := by
  sorry

end DiazModulus

Source

Standard. Formal proof: Diaz modulus mission, 1 October 2026 (C. Perassi).

View graph