mathlib3

04e80bb7 - refactor(number_theory/liouville/liouville_number): review API, golf (#19126)

refactor(number_theory/liouville/liouville_number): review API, golf (#19126) * Protect `liouville.irrational` and `liouville.transcendental`. * Sync file name with definition name (Liouville constant vs Liouville number). * Move auxiliary definitions and lemmas about Liouville number to `liouville_number` namespace. * Rename auxiliary definitions, golf proofs (where it doesn't affect readability).