mathlib3

781cc63f - feat(data/real/liouville, ring_theory/algebraic): a Liouville number is transcendental! (#6204)

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! Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>