Commit 2021-02-16 23:59 781cc63f

View on Github →

feat(data/real/liouville, ring_theory/algebraic): a Liouville number is transcendental! (#6204) This is an annotated proof. It finishes the first half of the Liouville PR. A taste of what is to come in a future PR: a proof that Liouville numbers actually exist!

Estimated changes

Modified src/data/real/liouville.lean

deleted theorem exists_one_le_pow_mul_dist

deleted theorem exists_pos_real_of_irrational_root

added theorem liouville.exists_one_le_pow_mul_dist

added theorem liouville.exists_pos_real_of_irrational_root

modified theorem liouville.irrational

added theorem liouville.transcendental

Modified src/ring_theory/algebraic.lean

added def transcendental