Structures · Topology
ContinuousSMul
Class ContinuousSMul M X says that the scalar multiplication (•) : M → X → X
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.
- Defined in
- Mathlib.Topology.Algebra.MulAction
- Shape
- 2 explicit arguments · adds continuous_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances17
- Int
- Nat
- Real
- Rat
- NNReal
- NNRat
- DomMulAct
- Units
- Matrix.SpecialLinearGroup
- Circle
- CategoryTheory.Aut
- Matrix.GeneralLinearGroup
- Subtype
- OrderDual
- Set.Elem
- ULift
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by1,091
- HasDerivAt
- HasDerivWithinAt
- HasStrictDerivAt
- ContinuousLinearMap.toSpanSingleton
- ContinuousLinearMap.smulRight
- HasFDerivAt.fderiv
- HasDerivAt.congr_simp
- HasFDerivWithinAt.fderivWithin
- uniqueDiffOn_univ
- HasDerivAtFilter
- Continuous.fun_smul
- LinearMap.toContinuousLinearMap
- HasStrictDerivAt.congr_simp
- DifferentiableOn.continuousOn
- Path.segment
- FiniteDimensional.complete
- HasDerivWithinAt.congr_simp
- continuous_algebraMap
- Differentiable.continuous
- DifferentiableAt.continuousAt
- HasDerivAt.hasFDerivAt
- NormedSpace.expSeries_radius_eq_top
- HasDerivWithinAt.hasFDerivWithinAt
- LinearEquiv.toContinuousLinearEquiv
- Filter.Tendsto.smul
- ContRepresentation.coind₁
- HasStrictDerivAt.hasStrictFDerivAt
- ContinuousSMul.continuous_smul
- TopRep.ofHom
- MvPowerSeries.aeval
- HasStrictFDerivAt.hasStrictDerivAt
- HasFDerivAt.hasDerivAt
- Module.Basis.equivFunL
- LinearMap.continuous_of_finiteDimensional
- Continuous.smul
- toEuclidean
- CovariantDerivative.toFun
- uniqueDiffWithinAt_univ
- absorbent_nhds_zero
- IsOpen.uniqueDiffOn
- LinearPMap.closure
- ContinuousOn.smul
- LinearPMap.IsClosable
- Convex.isPreconnected
- HasFDerivWithinAt.continuousWithinAt
- MeasureTheory.AEStronglyMeasurable.smul
- HasFDerivWithinAt.hasDerivWithinAt
- ContinuousAlternatingMap.apply
- TopRep.of
- ContinuousMultilinearMap.apply
Ancestors0
No ancestors.