feat: add ContinuousSMul instances for ℚ≥0

[astrainfinita]

---

[astrainfinita]

!bench

[github-actions]

PR summary 5c98c223ad

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Instances.Rat	1193	1195	+2 (+0.17%)

Import changes for all files

Files	Import difference
414 files Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomialDef Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.ConvergenceRadius Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Order Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Completion Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.Operations Mathlib.Analysis.Calculus.ContDiff.RestrictScalars Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.CompMul Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.CompCLM Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Congr Mathlib.Analysis.Calculus.FDeriv.Const Mathlib.Analysis.Calculus.FDeriv.Defs Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Pow Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.LinearIsometry Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Distribution.ContDiffMapSupportedIn Mathlib.Analysis.LConvolution Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Meromorphic.Basic Mathlib.Analysis.Meromorphic.Divisor Mathlib.Analysis.Meromorphic.IsolatedZeros Mathlib.Analysis.Meromorphic.NormalForm Mathlib.Analysis.Meromorphic.Order Mathlib.Analysis.Meromorphic.TrailingCoefficient Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Field.WithAbs Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Module.Ball.Action Mathlib.Analysis.Normed.Module.Ball.Homeomorph Mathlib.Analysis.Normed.Module.Ball.Pointwise Mathlib.Analysis.Normed.Module.Ball.RadialEquiv Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Convex Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.RCLike.Real Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Operator.Asymptotics Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.Basic Mathlib.Analysis.Normed.Operator.Bilinear Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact Mathlib.Analysis.Normed.Operator.Completeness Mathlib.Analysis.Normed.Operator.Conformal Mathlib.Analysis.Normed.Operator.Mul Mathlib.Analysis.Normed.Operator.NNNorm Mathlib.Analysis.Normed.Operator.NormedSpace Mathlib.Analysis.Normed.Operator.Prod Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.Units Mathlib.Analysis.NormedSpace.Alternating.Basic Mathlib.Analysis.NormedSpace.Alternating.Curry Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin Mathlib.Analysis.NormedSpace.BallAction Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.NormedSpace.Connected Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.NormedSpace.Extr Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Analysis.Real.OfDigits Mathlib.Analysis.Seminorm Mathlib.Analysis.SpecialFunctions.Choose Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecificLimits.Fibonacci Mathlib.Analysis.SpecificLimits.Normed Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Small Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Function Mathlib.FieldTheory.Galois.Profinite Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.Lebesgue.Add Mathlib.MeasureTheory.Integral.Lebesgue.Basic Mathlib.MeasureTheory.Integral.Lebesgue.Countable Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence Mathlib.MeasureTheory.Integral.Lebesgue.Map Mathlib.MeasureTheory.Integral.Lebesgue.Markov Mathlib.MeasureTheory.Integral.Lebesgue.MeasurePreserving Mathlib.MeasureTheory.Integral.Lebesgue.Norm Mathlib.MeasureTheory.Integral.Lebesgue.Sub Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Support Mathlib.MeasureTheory.Measure.Tight Mathlib.MeasureTheory.Measure.WithDensity Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.TsumDivsorsAntidiagonal Mathlib.Probability.Decision.Risk.Defs Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Kernel Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.CompMap Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.CompProd Mathlib.Probability.Kernel.Composition.Comp Mathlib.Probability.Kernel.Composition.KernelLemmas Mathlib.Probability.Kernel.Composition.Lemmas Mathlib.Probability.Kernel.Composition.MapComap Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.MeasureComp Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.Composition.Prod Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.WittVector.Compare Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.PerfectSpace Mathlib.Topology.Algebra.Module.StrongDual Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.CWComplex.Classical.Finite Mathlib.Topology.CWComplex.Classical.Subcomplex Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling.Basic Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Span Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Bounded.Normed Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.Instances.RatLemmas Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.Topology.MetricSpace.UniformConvergence Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.Lemmas Mathlib.Topology.Separation.NotNormal Mathlib.Topology.TietzeExtension Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.Hom	1
3 files Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.UniformSpace.CompareReals	2

---

Declarations diff

+ instance : ContinuousSMul ℚ ℝ
+ instance : ContinuousSMul ℚ≥0 NNReal
+ instance {R : Type*} [Ring R] [MulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :

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).

[themathqueen]

Is the Algebra ℚ≥0 R hypothesis necessary? Why not show it within the proof for continuous_smul?

[astrainfinita]

The argument of ContinuousSMul ℚ≥0 R needs Algebra ℚ≥0 R. Obtaining it from Algebra ℚ R will cause a diamond.

[themathqueen]

ah, fair enough

[ocfnash]

I don't agree with the claim about the diamond (in fact I claim the opposite!) but it doesn't matter since I have another suggestion.

[astrainfinita]

I think the diamond already exists. Zulip

[ocfnash]

This already exists via IsBoundedSMul.continuousSMul.

It's not out of the question to add a shortcut instance here but it would be helpful to hear the motivation.

[ocfnash]

I see you have not replied to this comment so I have made a suggestion myself instead.

[ocfnash]

I don't agree with the claim about the diamond (in fact I claim the opposite!) but it doesn't matter since I have another suggestion.

[ocfnash]

Note that via NNRat.instDistribMulActionOfRat we already have an action of ℚ≥0 on R so there is no need to include a typeclass carrying this. Also the Algebra assumption is more than we need and can be weakened to just DistribMulAction. Here is what I suggest:

Suggested change

	instance {R} [Ring R] [TopologicalSpace R] [Algebra ℚ R] [Algebra ℚ≥0 R] [ContinuousSMul ℚ R] :
	ContinuousSMul ℚ≥0 R where
	continuous_smul := by
	convert continuous_induced_dom.fst'.smul (M := ℚ) (X := R) continuous_snd using 2
	rw [← cast_smul_eq_nnqsmul ℚ]
	rfl
	instance {R : Type*} [Ring R] [DistribMulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :
	ContinuousSMul ℚ≥0 R where
	continuous_smul := continuous_induced_dom.fst'.smul continuous_snd

[leanprover-community-mathlib4-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 94eb313.
The entire run failed.
Found no significant differences.

[ocfnash]

I've left some suggestions; feel free to revert to your original design if these give trouble.

Thanks!

bors d+

[ocfnash]

Let's add the following, which I think is sufficient justification:

Suggested change

	instance : ContinuousSMul ℚ ℝ where
	-- Special case of `IsBoundedSMul.continuousSMul` but this shortcut instance reduces dependencies
	instance : ContinuousSMul ℚ ℝ where

[ocfnash]

I see you have not replied to this comment so I have made a suggestion myself instead.

[ocfnash]

Now that I realise NNRat.instMulActionOfRat is harmful, I realise that we should not author new lemmas about it (indeed we should excise it).

Thus your original design in which both the data of the ℚ≥0 and ℚ` actions were supplied was the right approach. Looking now I suppose we can generalise it slightly as follows:

Suggested change

	instance {R : Type*} [Ring R] [MulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :
	ContinuousSMul ℚ≥0 R where
	continuous_smul := continuous_induced_dom.fst'.smul continuous_snd
	instance {R : Type*} [SMul ℚ≥0 R] [MulAction ℚ R] [IsScalarTower ℚ≥0 ℚ R]
	[TopologicalSpace R] [ContinuousSMul ℚ R] :
	ContinuousSMul ℚ≥0 R where
	continuous_smul := by
	convert continuous_induced_dom.fst'.smul (M := ℚ) (X := R) continuous_snd using 2 with
	⟨⟨q, hq⟩, r⟩
	conv_lhs => rw [← one_smul ℚ r, ← smul_assoc]
	simp

(Note that for this to apply in the lemma below, we will need to add import Mathlib.Algebra.Module.Rat so that Lean can find IsScalarTower ℚ≥0 ℚ ℝ, and of course we should now drop import Mathlib.Data.NNRat.Lemmas.)

Apologies for the suggesting we use the bad instance.

[mathlib-bors]

✌️ astrainfinita can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.