Commit 2024-03-07 06:34 c8e50e0c

View on Github →

chore: Rename monotonicity of / lemmas (#10634) The new names and argument orders match the corresponding * lemmas, which I already took care of in a previous PR. From LeanAPAP

Estimated changes

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

Modified Mathlib/Algebra/Order/Field/Basic.lean

modified theorem div_le_div_of_le

deleted theorem div_le_div_of_le_left

deleted theorem div_le_div_of_le_of_nonneg

added theorem div_le_div_of_nonneg_left

added theorem div_le_div_of_nonneg_right

deleted theorem div_lt_div_of_lt

deleted theorem div_lt_div_of_lt_left

added theorem div_lt_div_of_pos_left

added theorem div_lt_div_of_pos_right

added theorem div_pos_iff_of_pos_left

added theorem div_pos_iff_of_pos_right

added theorem monotone_div_right_of_nonneg

added theorem strictMono_div_right_of_pos

Modified Mathlib/Algebra/Order/Field/Power.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

Modified Mathlib/Analysis/Convex/Strong.lean

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

Modified Mathlib/Analysis/NormedSpace/AddTorsor.lean

Modified Mathlib/Analysis/SpecialFunctions/Arsinh.lean

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

Modified Mathlib/Analysis/Subadditive.lean

Modified Mathlib/Combinatorics/Additive/Behrend.lean

Modified Mathlib/Combinatorics/Schnirelmann.lean

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

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

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

Modified Mathlib/Data/Real/NNReal.lean

Modified Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

Modified Mathlib/Topology/UrysohnsLemma.lean