Commit 2025-11-11 16:07 11acf7ca

View on Github →

chore(Analysis/SpecificLimits/Basic): generalize lemmas (#28475)

Estimated changes

Modified Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

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

Modified Mathlib/Analysis/PSeries.lean

Modified Mathlib/Analysis/Real/Hyperreal.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

Modified Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

added theorem NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat

added theorem NNRat.tendsto_inv_atTop_nhds_zero_nat

deleted theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat

deleted theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat

deleted theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat

deleted theorem Nat.tendsto_pow_atTop_atTop_of_one_lt

added theorem tendsto_add_mul_div_add_mul_atTop_nhds

added theorem tendsto_algebraMap_inv_atTop_nhds_zero_nat

deleted theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat

modified theorem tendsto_const_div_atTop_nhds_zero_nat

added theorem tendsto_inv_atTop_nhds_zero_nat

deleted theorem tendsto_inverse_atTop_nhds_zero_nat

modified theorem tendsto_natCast_div_add_atTop

modified theorem tendsto_one_div_add_atTop_nhds_zero_nat

modified theorem tendsto_one_div_atTop_nhds_zero_nat

Modified Mathlib/Analysis/SpecificLimits/RCLike.lean

deleted theorem RCLike.tendsto_add_mul_div_add_mul_atTop_nhds

deleted theorem RCLike.tendsto_inverse_atTop_nhds_zero_nat

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

Modified Mathlib/Dynamics/Ergodic/AddCircle.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean

Modified Mathlib/NumberTheory/Padics/Hensel.lean