Commit 2025-01-30 15:01 5b3fe125

View on Github →

chore(NumberTheory/LSeries): unsqueeze lots of terminal simps (#21133)

Estimated changes

Modified Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

Modified Mathlib/NumberTheory/LSeries/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Convergence.lean

modified theorem LSeries.abscissaOfAbsConv_le_one_of_isBigO_one

Modified Mathlib/NumberTheory/LSeries/Convolution.lean

Modified Mathlib/NumberTheory/LSeries/Deriv.lean

Modified Mathlib/NumberTheory/LSeries/Dirichlet.lean

Modified Mathlib/NumberTheory/LSeries/DirichletContinuation.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

modified theorem HurwitzZeta.oddKernel_zero

modified theorem HurwitzZeta.sinKernel_zero

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean

Modified Mathlib/NumberTheory/LSeries/Linearity.lean

Modified Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean