Commit 2023-06-01 05:11 04e80bb7
View on Github →refactor(number_theory/liouville/liouville_number): review API, golf (#19126)
- Protect
liouville.irrational
andliouville.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).