Commit 2025-05-23 23:59 de0f1e83

View on Github →

chore(*): use gcongr (#24720) Also add a few missing gcongr lemmas.

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Analysis/Asymptotics/ExpGrowth.lean

Modified Mathlib/Analysis/Asymptotics/LinearGrowth.lean

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/Analysis/Convex/Integral.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

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

added theorem ENNReal.log_le_log

added theorem ENNReal.log_lt_log

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

added theorem EReal.exp_le_exp

added theorem EReal.exp_lt_exp

Modified Mathlib/Data/EReal/Basic.lean

Modified Mathlib/Data/EReal/Inv.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Data/Nat/Factorial/Basic.lean

Modified Mathlib/NumberTheory/NumberField/House.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean