Structures · Algebra
LinearMap.CompatibleSMul
A typeclass for SMul structures which can be moved through a LinearMap.
This typeclass is generated automatically from an IsScalarTower instance, but exists so that
we can also add an instance for AddCommGroup.toIntModule, allowing z • to be moved even if
S does not support negation.
- Defined in
- Mathlib.Algebra.Module.LinearMap.Defs
- Shape
- 4 explicit arguments · adds map_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Finsupp
How is a type an instance?
Loading the hierarchy index…
Assumed by99
- LinearMap.restrictScalars
- ContinuousLinearMap.restrictScalars
- LinearMap.map_smul_of_tower
- LinearEquiv.restrictScalars
- LinearEquiv.restrictScalars_apply
- LinearMap.coe_restrictScalars
- LinearMap.restrictScalars_injective
- LinearEquiv.restrictScalars_toLinearMap
- LinearMap.compRight
- LinearMap.restrictScalarsₗ
- AlgHom.map_smul_of_tower
- LinearEquiv.multilinearMapCongrRight
- ContinuousLinearMap.map_smul_of_tower
- LinearMap.CompatibleSMul.map_smul
- ContinuousLinearMap.restrictScalars.congr_simp
- LinearMap.restrictScalars.congr_simp
- Derivation.restrictScalars
- LinearMap.restrictScalarsₗ_apply
- LinearMap.restrictScalars_apply
- LinearMapClass.map_smul_of_tower
- LinearMap.compMultilinearMapₗ
- LinearMap.comp_smul
- ContinuousLinearEquiv.restrictScalars
- ContinuousLinearMap.restrictScalarsₗ
- ContDiffMapSupportedIn.postcompLM
- LinearEquiv.multilinearMapCongrRight_symm_apply
- ContinuousLinearMap.coe_restrictScalars'
- StrictConvex.smul
- ContDiffMapSupportedIn.postcompCLM
- ContinuousLinearMap.comp_smul
- Derivation.map_smul_of_tower
- StrictConvexSpace.of_strictConvex_unitClosedBall
- LinearMap.isScalarTower_of_injective
- StrictConvex.linear_image
- LinearEquiv.restrictScalars_injective
- curveIntegralFun_restrictScalars
- ContIntertwiningMap.smul_comp
- curveIntegral_restrictScalars
- LinearMap.restrictScalars_inj
- LinearMap.restrictScalars_comp
- ContDiffMapSupportedIn.postcompLM_apply
- PositiveLinearMap.map_smul_of_tower
- LinearMap.compMultilinearMapₗ_apply
- LinearEquiv.restrictScalars_symm_apply
- ContIntertwiningMap.comp_smul
- LinearMap.compAlternatingMapₗ
- ContDiffMapSupportedIn.postcompLM.congr_simp
- LinearMap.restrictScalars_add
- ContIntertwiningMap.smul_apply
- LinearMap.restrictScalars_trans
Ancestors0
No ancestors.