chore(Analysis/SpecificLimits/Basic): generalize lemmas

[astrainfinita]

---

• depends on: [Merged by Bors] - chore(Topology/Algebra/Order/Field): generalize some lemmas to Semifield #28472
• depends on: feat: add ContinuousSMul instances for ℚ≥0 #28474

[github-actions]

PR summary 5c98c223ad

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.SpecificLimits.Basic	1446	1451	+5 (+0.35%)
Mathlib.Topology.Instances.Rat	1193	1194	+1 (+0.08%)

Import changes for all files

Files	Import difference
3 files Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.UniformSpace.CompareReals	1
85 files Mathlib.Algebra.ArithmeticGeometric Mathlib.Analysis.Asymptotics.LinearGrowth Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.Complex.Cardinality Mathlib.Analysis.Hofer Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Analysis.Real.Cardinality Mathlib.Analysis.Real.Hyperreal Mathlib.Analysis.SpecificLimits.ArithmeticGeometric Mathlib.Analysis.SpecificLimits.Basic Mathlib.Data.Complex.Cardinality Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Real.Cardinality Mathlib.Data.Real.Hyperreal Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.LinearAlgebra.Complex.FiniteDimensional Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.AddContent Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion Mathlib.MeasureTheory.Measure.Decomposition.Hahn Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Real Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses.Finite Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms Mathlib.MeasureTheory.Measure.Typeclasses.Probability Mathlib.MeasureTheory.Measure.Typeclasses.SFinite Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfAddContent Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.Topology Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan Mathlib.Probability.ConditionalProbability Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.UniformOn Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.GDelta.MetrizableSpace Mathlib.Topology.GDelta.UniformSpace Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.MetricSpace.PiNat Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.MetricSpace.Thickening	5

---

Declarations diff

+ NNRat.tendsto_algebraMap_inverse_atTop_nhds_zero_nat
+ NNRat.tendsto_inv_atTop_nhds_zero_nat
+ RCLike.tendsto_inverse_atTop_nhds_zero_nat
+ instance : ContinuousSMul ℚ ℝ
+ instance : ContinuousSMul ℚ≥0 NNReal
+ instance {R} [Ring R] [TopologicalSpace R] [Algebra ℚ R] [Algebra ℚ≥0 R] [ContinuousSMul ℚ R] :
+ tendsto_inv_atTop_nhds_zero_nat
+-- tendsto_inverse_atTop_nhds_zero_nat

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Topology/Algebra/Order/Field): generalize some lemmas to Semifield #28472
• feat: add ContinuousSMul instances for ℚ≥0 #28474
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.