Documentation Verification Report

Basic

📁 Source: Mathlib/NumberTheory/LSeries/Basic.lean

Statistics

Metric	Count
Definitions `LSeries`, `delta`, `termL`, `termδ`, `«term↗_»`, `term`, `LSeriesHasSum`, `LSeriesSummable`	8
Theorems `delta_mul`, `delta_mul_eq_smul_delta`, `eq_zero_of_not_LSeriesSummable`, `mul_delta`, `mul_delta_eq_smul_delta`, `norm_term_eq`, `norm_term_le`, `norm_term_le_of_re_le_re`, `pow_mul_term_eq`, `term_congr`, `term_def`, `term_def₀`, `term_delta`, `term_nonneg`, `term_of_ne_zero`, `term_of_ne_zero'`, `term_pos`, `term_zero`, `LSeriesSummable`, `LSeries_eq`, `LSeriesHasSum_congr`, `LSeriesHasSum_iff`, `LSeriesHasSum`, `congr'`, `isBigO_rpow`, `le_const_mul_rpow`, `of_re_le_re`, `LSeriesSummable_congr`, `LSeriesSummable_congr'`, `LSeriesSummable_iff_of_re_eq_re`, `LSeriesSummable_of_bounded_of_one_lt_re`, `LSeriesSummable_of_bounded_of_one_lt_real`, `LSeriesSummable_of_isBigO_rpow`, `LSeriesSummable_of_le_const_mul_rpow`, `LSeriesSummable_zero`, `LSeries_congr`, `LSeries_delta`, `LSeries_zero`	38
Total	46

LSeries

Definitions

Name	Category	Theorems
`delta` 📖	CompOp	11 math math: `DirichletCharacter.mul_delta`, `ArithmeticFunction.one_eq_delta`, `term_delta`, `LSeries_delta`, `mul_delta`, `mul_delta_eq_smul_delta`, `delta_mul`, `delta_mul_eq_smul_delta`, `DirichletCharacter.delta_mul`, `DirichletCharacter.convolution_mul_moebius`, `DirichletCharacter.modZero_eq_delta`
`term` 📖	CompOp	26 math math: `term_sum`, `term_convolution'`, `term_congr`, `term_def`, `term_sub`, `term_of_ne_zero`, `term_nonneg`, `term_convolution`, `norm_term_eq`, `term_sub_apply`, `term_neg_apply`, `term_delta`, `term_add_apply`, `term_neg`, `term_of_ne_zero'`, `term_add`, `term_smul_apply`, `term_pos`, `term_def₀`, `term_sum_apply`, `pow_mul_term_eq`, `term_smul`, `norm_term_le`, `hasDerivAt_term`, `term_zero`, `norm_term_le_of_re_le_re`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`delta_mul` 📖	mathematical	`Complex` `Complex.instOne`	`Pi.instMul` `Complex.instMul` `delta`	—	`mul_delta` `mul_comm`
`delta_mul_eq_smul_delta` 📖	mathematical	—	`Pi.instMul` `Complex` `Complex.instMul` `delta` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`mul_delta_eq_smul_delta` `mul_comm`
`eq_zero_of_not_LSeriesSummable` 📖	mathematical	`LSeriesSummable`	`LSeries` `Complex` `Complex.instZero`	—	`tsum_eq_zero_of_not_summable`
`mul_delta` 📖	mathematical	`Complex` `Complex.instOne`	`Pi.instMul` `Complex.instMul` `delta`	—	`mul_delta_eq_smul_delta` `one_smul`
`mul_delta_eq_smul_delta` 📖	mathematical	—	`Pi.instMul` `Complex` `Complex.instMul` `delta` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`mul_one` `MulZeroClass.mul_zero`
`norm_term_eq` 📖	mathematical	—	`Norm.norm` `Complex` `Complex.instNorm` `term` `Real` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instPow` `Real.instNatCast` `Complex.re`	—	`eq_or_ne` `norm_zero` `term_of_ne_zero` `Complex.norm_div` `Complex.norm_natCast_cpow_of_pos`
`norm_term_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm`	`term`	—	`norm_term_eq` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `le_of_lt` `Real.rpow_pos_of_pos` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `le_refl`
`norm_term_le_of_re_le_re` 📖	mathematical	`Real` `Real.instLE` `Complex.re`	`Norm.norm` `Complex` `Complex.instNorm` `term`	—	`norm_term_eq` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_nonneg` `le_refl` `Real.rpow_pos_of_pos` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `Real.rpow_le_rpow_of_exponent_le` `Nat.one_le_cast`
`pow_mul_term_eq` 📖	mathematical	—	`Complex` `Complex.instMul` `Complex.instPow` `Complex.instAdd` `Complex.instNatCast` `Complex.instOne` `term`	—	`Nat.cast_add` `Nat.cast_one` `mul_div_assoc'` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `Complex.natCast_add_one_cpow_ne_zero`
`term_congr` 📖	mathematical	—	`term`	—	`eq_or_ne` `term_of_ne_zero`
`term_def` 📖	mathematical	—	`term` `Complex` `Complex.instZero` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instPow` `Complex.instNatCast`	—	—
`term_def₀` 📖	mathematical	`Complex` `Complex.instZero`	`term` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg`	—	`term.eq_1` `CharP.cast_eq_zero` `CharP.ofCharZero` `Complex.instCharZero` `Complex.cpow_neg` `MulZeroClass.zero_mul` `div_eq_inv_mul` `mul_comm`
`term_delta` 📖	mathematical	—	`term` `delta` `Complex` `Complex.instOne` `Complex.instZero`	—	`eq_or_ne` `term_of_ne_zero` `Nat.cast_one` `Complex.one_cpow` `div_self` `NeZero.charZero_one` `Complex.instCharZero` `zero_div`
`term_nonneg` 📖	mathematical	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero`	`term` `Complex.ofReal`	—	`term_def` `le_rfl` `mul_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `RCLike.toIsStrictOrderedRing` `LT.lt.le` `Complex.inv_natCast_cpow_ofReal_pos`
`term_of_ne_zero` 📖	mathematical	—	`term` `Complex` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instPow` `Complex.instNatCast`	—	—
`term_of_ne_zero'` 📖	mathematical	—	`term` `Complex` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instPow` `Complex.instNatCast`	—	`eq_or_ne` `term_zero` `Nat.cast_zero` `Complex.zero_cpow` `div_zero` `term_of_ne_zero`
`term_pos` 📖	mathematical	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero`	`term` `Complex.ofReal`	—	`term_of_ne_zero` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `RCLike.toIsStrictOrderedRing` `Complex.inv_natCast_cpow_ofReal_pos`
`term_zero` 📖	mathematical	—	`term` `Complex` `Complex.instZero`	—	—

LSeries.notation

Definitions

Name	Category	Theorems
`termL` 📖	CompOp	—
`termδ` 📖	CompOp	—
`«term↗_»` 📖	CompOp	—

LSeriesHasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeriesSummable` 📖	mathematical	`LSeriesHasSum`	`LSeriesSummable`	—	`HasSum.summable`
`LSeries_eq` 📖	mathematical	`LSeriesHasSum`	`LSeries`	—	`HasSum.tsum_eq` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional`

LSeriesSummable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeriesHasSum` 📖	mathematical	`LSeriesSummable`	`LSeriesHasSum` `LSeries`	—	`Summable.hasSum`
`congr'` 📖	—	`Filter.EventuallyEq` `Complex` `Filter.atTop` `Nat.instPreorder` `LSeriesSummable`	—	—	`Summable.of_norm_bounded_eventually` `Complex.instCompleteSpace` `summable_norm_iff` `Complex.instFiniteDimensionalReal` `Filter.eventuallyEq_iff_exists_mem` `Nat.cofinite_eq_atTop` `Filter.diff_mem` `Set.Finite.compl_mem_cofinite` `Set.finite_singleton` `LSeries.term_of_ne_zero` `Set.mem_singleton_iff` `Set.mem_diff` `Filter.Eventually.mono` `Filter.EventuallyEq.symm`
`isBigO_rpow` 📖	mathematical	`LSeriesSummable`	`Asymptotics.IsBigO` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instPow` `Real.instNatCast` `Complex.re`	—	`le_const_mul_rpow` `Asymptotics.IsBigO.of_bound` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Real.norm_eq_abs` `Real.abs_rpow_of_nonneg` `Nat.cast_nonneg` `Real.instIsOrderedRing` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`le_const_mul_rpow` 📖	mathematical	`LSeriesSummable`	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Real.instMul` `Real.instPow` `Real.instNatCast` `Complex.re`	—	`Summable.norm` `Complex.instFiniteDimensionalReal` `Mathlib.Tactic.Push.not_forall_eq` `Summable.le_tsum` `Real.instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `norm_nonneg` `LT.lt.false` `LE.le.trans_lt` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Real.rpow_pos_of_pos` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `LSeries.norm_term_eq`
`of_re_le_re` 📖	—	`Real` `Real.instLE` `Complex.re` `LSeriesSummable`	—	—	`eq_1` `summable_norm_iff` `Complex.instFiniteDimensionalReal` `Summable.of_nonneg_of_le` `norm_nonneg` `LSeries.norm_term_le_of_re_le_re`

(root)

Definitions

Name	Category	Theorems
`LSeries` 📖	CompOp	62 math math: `DirichletCharacter.LSeries_eulerProduct_tprod`, `DirichletCharacter.LSeries_modOne_eq`, `LSeries_injOn`, `LSeries_eventually_eq_zero_iff'`, `DirichletCharacter.LSeries_twist_vonMangoldt_eq`, `DirichletCharacter.LFunction_eq_LSeries`, `DirichletCharacter.norm_LSeries_product_ge_one`, `ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius`, `LSeries_congr`, `DirichletCharacter.deriv_LFunction_eq_deriv_LSeries`, `LSeries_iteratedDeriv`, `ArithmeticFunction.LSeries_positive`, `ZMod.LFunction_eq_LSeries`, `LSeries_deriv_eqOn`, `LSeries_analyticOnNhd`, `LSeries_sub`, `LSeries_neg`, `LSeries_deriv`, `DirichletCharacter.LSeries_changeLevel`, `LSeries_smul`, `LSeries_eq_mul_integral_of_nonneg`, `ArithmeticFunction.LSeries_zeta_eq`, `DirichletCharacter.LSeries.mul_mu_eq_one`, `ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div`, `LSeriesSummable.LSeriesHasSum`, `LSeries_convolution'`, `ArithmeticFunction.LSeries_mul'`, `LSeries_one_eq_riemannZeta`, `LSeries_eq_mul_integral`, `ArithmeticFunction.LSeries_vonMangoldt_eq`, `LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg`, `LSeries_differentiableOn`, `LSeries_eq_iff_of_abscissaOfAbsConv_lt_top`, `LSeries_sum`, `LSeries.iteratedDeriv_alternating`, `LSeries_one_mul_Lseries_moebius`, `DirichletCharacter.LSeries_eulerProduct_hasProd`, `LSeries_add`, `LSeries_delta`, `tsum_dirichletSummand`, `ArithmeticFunction.LSeries_zeta_eq_riemannZeta`, `DirichletCharacter.LSeries_eulerProduct_exp_log`, `LSeries.tendsto_cpow_mul_atTop`, `ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq`, `LSeries.positive`, `ArithmeticFunction.LSeries_mul`, `LSeries.tendsto_atTop`, `LSeries_zero`, `LSeries_analyticOn`, `ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log`, `LSeries_eq_zero_of_abscissaOfAbsConv_eq_top`, `LSeriesHasSum.LSeries_eq`, `LSeries_hasDerivAt`, `ArithmeticFunction.iteratedDeriv_LSeries_alternating`, `LSeries.eq_zero_of_not_LSeriesSummable`, `DirichletCharacter.LSeries_eulerProduct`, `ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux`, `LSeries_eq_zero_iff`, `LSeries_eq_mul_integral'`, `LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div`, `LSeries_convolution`, `LSeriesHasSum_iff`
`LSeriesHasSum` 📖	MathDef	8 math math: `HurwitzZeta.LSeriesHasSum_cos`, `LSeriesHasSum_congr`, `LSeriesSummable.LSeriesHasSum`, `HurwitzZeta.LSeriesHasSum_exp`, `LSeriesHasSum_one`, `ArithmeticFunction.LSeriesHasSum_zeta`, `HurwitzZeta.LSeriesHasSum_sin`, `LSeriesHasSum_iff`
`LSeriesSummable` 📖	MathDef	28 math math: `LSeriesSummable_of_le_const_mul_rpow`, `LSeriesSummable_congr'`, `DirichletCharacter.LSeriesSummable_of_one_lt_re`, `ArithmeticFunction.not_LSeriesSummable_moebius_at_one`, `LSeriesSummable_of_bounded_of_one_lt_real`, `LSeriesSummable_zero`, `LSeriesSummable_congr`, `LSeriesSummable.neg_iff`, `LSeriesSummable_of_isBigO_rpow`, `DirichletCharacter.LSeriesSummable_twist_vonMangoldt`, `DirichletCharacter.LSeriesSummable_iff`, `LSeriesSummable.smul_iff`, `LSeriesSummable_of_abscissaOfAbsConv_lt_re`, `LSeriesSummable_of_bounded_of_one_lt_re`, `LSeriesSummable_iff_of_re_eq_re`, `LSeriesSummable_one_iff`, `LSeriesSummable_of_sum_norm_bigO`, `ZMod.LSeriesSummable_of_one_lt_re`, `ArithmeticFunction.LSeriesSummable_moebius_iff`, `LSeriesSummable_of_sum_norm_bigO_and_nonneg`, `ArithmeticFunction.LSeriesSummable_zeta_iff`, `LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re`, `DirichletCharacter.not_LSeriesSummable_at_one`, `LSeriesHasSum.LSeriesSummable`, `ArithmeticFunction.LSeriesSummable_vonMangoldt`, `DirichletCharacter.LSeriesSummable_zetaMul`, `LSeriesSummable_logMul_of_lt_re`, `LSeriesHasSum_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeriesHasSum_congr` 📖	mathematical	—	`LSeriesHasSum`	—	`LSeriesSummable_congr` `LSeries_congr`
`LSeriesHasSum_iff` 📖	mathematical	—	`LSeriesHasSum` `LSeriesSummable` `LSeries`	—	`LSeriesHasSum.LSeriesSummable` `LSeriesHasSum.LSeries_eq` `LSeriesSummable.LSeriesHasSum`
`LSeriesSummable_congr` 📖	mathematical	—	`LSeriesSummable`	—	`summable_congr` `LSeries.term_congr`
`LSeriesSummable_congr'` 📖	mathematical	`Filter.EventuallyEq` `Complex` `Filter.atTop` `Nat.instPreorder`	`LSeriesSummable`	—	`LSeriesSummable.congr'` `Filter.EventuallyEq.symm`
`LSeriesSummable_iff_of_re_eq_re` 📖	mathematical	`Complex.re`	`LSeriesSummable`	—	`LSeriesSummable.of_re_le_re` `Eq.le`
`LSeriesSummable_of_bounded_of_one_lt_re` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Real.instLT` `Real.instOne` `Complex.re`	`LSeriesSummable`	—	`LSeriesSummable_of_le_const_mul_rpow` `sub_self` `Real.rpow_zero` `mul_one`
`LSeriesSummable_of_bounded_of_one_lt_real` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Real.instLT` `Real.instOne`	`LSeriesSummable` `Complex.ofReal`	—	`LSeriesSummable_of_bounded_of_one_lt_re`
`LSeriesSummable_of_isBigO_rpow` 📖	mathematical	`Real` `Real.instLT` `Complex.re` `Asymptotics.IsBigO` `Complex` `Complex.instNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instPow` `Real.instNatCast` `Real.instSub` `Real.instOne`	`LSeriesSummable`	—	`Asymptotics.isBigO_iff` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Finset.insert_nonempty` `LE.le.trans` `Finset.mem_insert` `Finset.le_max'` `le_max_right` `le_max_left` `LSeriesSummable_of_le_const_mul_rpow` `le_or_gt` `Nat.cast_nonneg` `Real.instIsOrderedRing` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Real.norm_eq_abs` `Real.abs_rpow_of_nonneg` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_refl` `norm_nonneg` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Real.rpow_pos_of_pos` `Nat.cast_pos` `Real.instNontrivial` `Finset.mem_insert_of_mem` `Finset.mem_image` `Finset.mem_range`
`LSeriesSummable_of_le_const_mul_rpow` 📖	mathematical	`Real` `Real.instLT` `Complex.re` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Real.instMul` `Real.instPow` `Real.instNatCast` `Real.instSub` `Real.instOne`	`LSeriesSummable`	—	`LE.le.trans` `norm_nonneg` `Nat.cast_one` `Real.one_rpow` `mul_one` `one_ne_zero` `div_eq_mul_inv` `norm_mul` `NormedDivisionRing.toNormMulClass` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Summable.of_norm_bounded_eventually_nat` `Real.instCompleteSpace` `norm_norm` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `le_of_eq` `Complex.norm_natCast_cpow_of_pos` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_neg` `add_zero` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.add_neg` `Summable.of_norm` `Complex.instCompleteSpace` `Summable.of_nonneg_of_le` `norm_zero` `Real.rpow_pos_of_pos` `Nat.cast_pos` `Real.instNontrivial` `LSeries.term_of_ne_zero` `LT.lt.ne'` `norm_div` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Complex.norm_real` `Real.norm_of_nonneg` `mul_assoc` `Real.rpow_neg` `Nat.cast_nonneg` `Real.rpow_add` `neg_add_rev` `neg_sub` `neg_add_cancel_right`
`LSeriesSummable_zero` 📖	mathematical	—	`LSeriesSummable` `Pi.instZero` `Complex` `Complex.instZero`	—	`LSeries.term_def` `zero_div`
`LSeries_congr` 📖	mathematical	—	`LSeries`	—	`tsum_congr` `LSeries.term_congr`
`LSeries_delta` 📖	mathematical	—	`LSeries` `LSeries.delta` `Pi.instOne` `Complex` `Complex.instOne`	—	`LSeries.term_delta` `tsum_ite_eq` `SummationFilter.instLeAtTopUnconditional`
`LSeries_zero` 📖	mathematical	—	`LSeries` `Pi.instZero` `Complex` `Complex.instZero`	—	`zero_div` `tsum_zero`

---

← Back to Index