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

Modified docs/overview.yaml

Modified src/number_theory/liouville/basic.lean

deleted theorem liouville.irrational

deleted theorem liouville.transcendental

Renamed src/number_theory/liouville/liouville_constant.lean to src/number_theory/liouville/liouville_number.lean

deleted theorem liouville.aux_calc

deleted theorem liouville.is_liouville

deleted theorem liouville.is_transcendental

deleted def liouville.liouville_number

deleted theorem liouville.liouville_number_eq_initial_terms_add_tail

deleted def liouville.liouville_number_initial_terms

deleted theorem liouville.liouville_number_rat_initial_terms

deleted def liouville.liouville_number_tail

deleted theorem liouville.liouville_number_tail_pos

deleted theorem liouville.tsum_one_div_pow_factorial_lt

added theorem liouville_liouville_number

added theorem liouville_number.aux_calc

added def liouville_number.partial_sum

added theorem liouville_number.partial_sum_add_remainder

added theorem liouville_number.partial_sum_eq_rat

added theorem liouville_number.partial_sum_succ

added def liouville_number.remainder

added theorem liouville_number.remainder_lt'

added theorem liouville_number.remainder_lt

added theorem liouville_number.remainder_pos

added theorem liouville_number.remainder_summable

added def liouville_number

added theorem transcendental_liouville_number