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

Proved

Transcendence.quadratic_coeffs_eq_zero_of_transcendental

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

diaz-modulus-leannumber-theorytranscendence

Let $x \in \mathbb{C}$ be transcendental, and let $c_0, c_1, c_2 \in \mathbb{C}$ be algebraic. If

c_2 x^{2} + c_1 x + c_0 = 0,

then $c_2 = c_1 = c_0 = 0$ .

It is used at $x = \pi$ and $x = \pi^{2}$ , where it turns a relation with algebraic coefficients into three separate equations.

Preamble

import Mathlib

Formal statement

namespace Transcendence

theorem quadratic_coeffs_eq_zero_of_transcendental {x c₀ c₁ c₂ : ℂ} (hx : Transcendental ℚ x)
    (h₀ : IsAlgebraic ℚ c₀) (h₁ : IsAlgebraic ℚ c₁) (h₂ : IsAlgebraic ℚ c₂)
    (h : c₂ * x ^ 2 + c₁ * x + c₀ = 0) :
    c₂ = 0 ∧ c₁ = 0 ∧ c₀ = 0 := by
  sorry

end Transcendence

Source

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

View graph