Champernowne's theorem (1933)

The base-b Champernowne sequence is normal in base b.

theorem Champernowne.champernowne_normal (b : ℕ) (hb : 2 ≤ b) : IsNormalSequence b (champDigit b)

theorem Champernowne.champernowne_normal_ten : IsNormalSequence 10 (champDigit 10)

The classical base-10 statement.