liouville_transcendental_explicit
Provednumber-theoryprovedtranscendence-theory
Liouville's constant: ∑ 10^{-n!} is transcendental (first proved transcendental number, Liouville 1851). More generally, any Liouville number is transcendental.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem liouville_transcendental_explicit :
Transcendental ℚ (∑' n : ℕ, (1 : ℝ) / 10 ^ (n.factorial)) := by
sorrySource