Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-01 05:11 04e80bb7

View on Github →

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).

Estimated changes