Commit 2025-02-19 08:59 0a431397

View on Github →

chore(AtTop/Monoid): add multiplicative versions (#21878) Also review names in the file. Moves:

Filter.Tendsto.atTop_mul_atTop ->Filter.Tendsto.atTop_mul_atTop₀
Filter.Tendsto.atBot_mul_atBot ->Filter.Tendsto.atBot_mul_atBot₀
Filter.Tendsto.atTop_of_mul_const -> Filter.Tendsto.atTop_of_mul_const₀
Filter.Tendsto.atTop_of_const_mul -> Filter.Tendsto.atTop_of_const_mul₀

Estimated changes

Modified Mathlib/Algebra/QuadraticDiscriminant.lean

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean

Modified Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

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

Modified Mathlib/Order/Filter/AtTopBot/Field.lean

Modified Mathlib/Order/Filter/AtTopBot/Group.lean

Modified Mathlib/Order/Filter/AtTopBot/Monoid.lean

added theorem Filter.Tendsto.atBot_mul_atBot

added theorem Filter.Tendsto.atBot_mul_eventuallyLE_one

added theorem Filter.Tendsto.atBot_mul_le_one

added theorem Filter.Tendsto.atBot_of_const_le_mul

added theorem Filter.Tendsto.atBot_of_const_mul

added theorem Filter.Tendsto.atBot_of_isBoundedUnder_ge_mul

added theorem Filter.Tendsto.atBot_of_mul_const

added theorem Filter.Tendsto.atBot_of_mul_const_le

added theorem Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge

added theorem Filter.Tendsto.atBot_pow

added theorem Filter.Tendsto.atTop_mul_atTop

added theorem Filter.Tendsto.atTop_mul_one_eventuallyLE

added theorem Filter.Tendsto.atTop_mul_one_le

added theorem Filter.Tendsto.atTop_of_const_mul

added theorem Filter.Tendsto.atTop_of_isBoundedUnder_le_mul

added theorem Filter.Tendsto.atTop_of_le_const_mul

added theorem Filter.Tendsto.atTop_of_mul_const

added theorem Filter.Tendsto.atTop_of_mul_isBoundedUnder_le

added theorem Filter.Tendsto.atTop_of_mul_le_const

added theorem Filter.Tendsto.atTop_pow

added theorem Filter.Tendsto.eventuallyLE_one_mul_atBot

added theorem Filter.Tendsto.le_one_mul_atBot

deleted theorem Filter.Tendsto.nsmul_atBot

deleted theorem Filter.Tendsto.nsmul_atTop

added theorem Filter.Tendsto.one_eventuallyLE_mul_atTop

added theorem Filter.Tendsto.one_le_mul_atTop

deleted theorem Filter.tendsto_atBot_add

deleted theorem Filter.tendsto_atBot_add_nonpos_left'

deleted theorem Filter.tendsto_atBot_add_nonpos_left

deleted theorem Filter.tendsto_atBot_add_nonpos_right'

deleted theorem Filter.tendsto_atBot_add_nonpos_right

deleted theorem Filter.tendsto_atBot_of_add_const_left

deleted theorem Filter.tendsto_atBot_of_add_const_right

deleted theorem Filter.tendsto_atTop_add

deleted theorem Filter.tendsto_atTop_add_nonneg_left'

deleted theorem Filter.tendsto_atTop_add_nonneg_left

deleted theorem Filter.tendsto_atTop_add_nonneg_right'

deleted theorem Filter.tendsto_atTop_add_nonneg_right

deleted theorem Filter.tendsto_atTop_of_add_const_left

deleted theorem Filter.tendsto_atTop_of_add_const_right

Modified Mathlib/Order/Filter/AtTopBot/Ring.lean

deleted theorem Filter.Tendsto.atBot_mul_atBot

added theorem Filter.Tendsto.atBot_mul_atBot₀

deleted theorem Filter.Tendsto.atBot_mul_atTop

added theorem Filter.Tendsto.atBot_mul_atTop₀

deleted theorem Filter.Tendsto.atTop_mul_atBot

added theorem Filter.Tendsto.atTop_mul_atBot₀

deleted theorem Filter.Tendsto.atTop_mul_atTop

added theorem Filter.Tendsto.atTop_mul_atTop₀

deleted theorem Filter.Tendsto.atTop_of_const_mul

added theorem Filter.Tendsto.atTop_of_const_mul₀

deleted theorem Filter.Tendsto.atTop_of_mul_const

added theorem Filter.Tendsto.atTop_of_mul_const₀

Modified Mathlib/Topology/Algebra/Polynomial.lean