Commit 2024-11-18 07:12 a2d097b7

View on Github →

chore: more uses of calc and gcongr (#19173) Motivated by the deprecation in #19081

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

added theorem pow_left_monotoneOn

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/Normed/Field/Ultra.lean

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Real/Archimedean.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Real/Pi/Bounds.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

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

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean