Commit 2023-05-30 09:54 12c5da0f

View on Github →

feat: port NumberTheory.LSeries (#4495)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LSeries.lean

added def Nat.ArithmeticFunction.LSeries

added def Nat.ArithmeticFunction.LSeriesSummable

added theorem Nat.ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re

added theorem Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re

added theorem Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real

added theorem Nat.ArithmeticFunction.LSeriesSummable_zero

added theorem Nat.ArithmeticFunction.LSeries_add

added theorem Nat.ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable

added theorem Nat.ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re