Commit 2025-06-03 10:13 1afce00c

View on Github →

chore(Analysis/Normed/Group/InfiniteSum): make argument implicit (#25375) Make an argument g which is followed by an explicit hypothesis hg about g implicit. And make one minor tweak to the file, tidying after #25371.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Analysis/Analytic/OfScalars.lean

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Modified Mathlib/Analysis/Calculus/SmoothSeries.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

modified theorem Summable.of_nnnorm_bounded

modified theorem Summable.of_norm_bounded

modified theorem Summable.of_norm_bounded_eventually

modified theorem Summable.of_norm_bounded_eventually_nat

modified theorem cauchySeq_finset_of_norm_bounded

modified theorem cauchySeq_range_of_norm_bounded

Modified Mathlib/Analysis/Normed/Group/Tannery.lean

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/NumberTheory/LSeries/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Deriv.lean

Modified Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean

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

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