Structures · Topology
ContinuousConstSMul
Class ContinuousConstSMul Γ T says that the scalar multiplication (•) : Γ → T → T
is continuous in the second argument. We use the same class for all kinds of multiplicative
actions, including (semi)modules and algebras.
Note that both ContinuousConstSMul α α and ContinuousConstSMul αᵐᵒᵖ α are
weaker versions of ContinuousMul α.
- Defined in
- Mathlib.Topology.Algebra.ConstMulAction
- Shape
- 2 explicit arguments · adds continuous_const_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances11
- Int
- Nat
- Rat
- ContinuousLinearMap
- Units
- ConjAct
- Matrix.GeneralLinearGroup
- Subtype
- OrderDual
- ULift
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by1,207
- FormalMultilinearSeries
- WeakDual
- Submodule.topologicalClosure
- WeakDual.characterSpace
- FormalMultilinearSeries.compContinuousLinearMap
- FormalMultilinearSeries.sum
- FormalMultilinearSeries.partialSum
- TemperedDistribution.smulLeftCLM
- ContinuousLinearMap.toLinearMap₁₂
- ContinuousConstSMul.continuous_const_smul
- FormalMultilinearSeries.comp
- topDualPairing
- FormalMultilinearSeries.applyComposition
- Homeomorph.smul
- WeakDual.toStrongDual
- StrongDual.toWeakDual
- NonUnitalStarAlgebra.elemental
- FormalMultilinearSeries.compAlongComposition
- Continuous.const_smul
- ContinuousLinearMap.postcomp
- ContinuousLinearMap.compFormalMultilinearSeries
- StrongDual.extendRCLikeₗ
- constFormalMultilinearSeries
- StrongDual.extendRCLike
- Submodule.closure
- ContinuousLinearEquiv.arrowCongr
- WeakSpace
- Convex.interior
- FormalMultilinearSeries.restrictScalars
- ContinuousLinearMap.precomp
- ContinuousMultilinearMap.compContinuousLinearMapL
- FormalMultilinearSeries.order
- Filter.Tendsto.const_smul
- Continuous.fun_const_smul
- FormalMultilinearSeries.pi
- ContinuousAlternatingMap.apply
- ContinuousMultilinearMap.apply
- ContinuousAlternatingMap.compContinuousLinearMapCLM
- NonUnitalStarSubalgebra.topologicalClosure
- TemperedDistribution.smulLeftCLM_apply_apply
- Homeomorph.smulOfNeZero
- toWeakSpace
- MeasureTheory.AEStronglyMeasurable.const_smul
- SeparationQuotient.outCLM
- HasSum.const_smul
- ContinuousLinearEquiv.conjContinuousAlgEquiv
- ContinuousOn.fun_const_smul
- set_smul_mem_nhds_zero_iff
- FormalMultilinearSeries.congr
- WeakDual.extendRCLikeL
Ancestors0
No ancestors.