Commit 2025-01-02 11:03 d458ec9a

View on Github →

feat(NumberTheory/LSeries/Injectivity): new file (#20370) This adds the statement that a converging L-series determines its coefficients.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

added theorem Complex.cpow_natCast_add_one_ne_zero

Modified Mathlib/NumberTheory/LSeries/Basic.lean

added theorem LSeries.pow_mul_term_eq

Modified Mathlib/NumberTheory/LSeries/Convergence.lean

added theorem LSeries.abscissaOfAbsConv_binop_le

Modified Mathlib/NumberTheory/LSeries/Convolution.lean

added theorem LSeries.abscissaOfAbsConv_convolution_le

Created Mathlib/NumberTheory/LSeries/Injectivity.lean

added theorem LSeries.abscissaOfAbsConv_add_le

added theorem LSeries.abscissaOfAbsConv_sub_le

added theorem LSeries.eq_of_LSeries_eventually_eq

added theorem LSeries.tendsto_atTop

added theorem LSeries.tendsto_cpow_mul_atTop

added theorem LSeries_eq_iff_of_abscissaOfAbsConv_lt_top

added theorem LSeries_eq_zero_iff

added theorem LSeries_eq_zero_of_abscissaOfAbsConv_eq_top

added theorem LSeries_eventually_eq_zero_iff'

added theorem LSeries_injOn

added theorem LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq

added theorem cpow_mul_div_cpow_eq_div_div_cpow