Structures · Data types
IsSMulApply
IsSMulApply M F α β states for all f : F, n : M and x : α, (n • f) x = n • f x.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Shape
- 4 explicit arguments · adds smul_apply
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by66
- smul_apply
- FunLike.coe_smul
- FunLike.natCast_eq_nsmul_one
- IsSMulApply.smul_apply
- FunLike.intCast_eq_zsmul_one
- FunLike.addRightCancelMonoid
- FunLike.semiring
- GroupSeminorm.smul_apply
- CuspForm.IsGLPos.smul_apply
- SlashInvariantForm.coe_smulℝ
- FunLike.subNegMonoid
- FunLike.addCommGroup
- MeasureTheory.OuterMeasure.smul_apply
- Seminorm.smul_apply
- FunLike.subtractionCommMonoid
- FunLike.addGroup
- ContDiffMapSupportedIn.coe_smul
- FunLike.isScalarTower
- ProbabilityTheory.Kernel.nsmul_apply
- FunLike.module
- Seminorm.coe_smul
- ContinuousLinearMap.coe_smul'
- TestFunction.coe_smul
- NonarchAddGroupSeminorm.coe_smul
- AddGroupSeminorm.smul_apply
- FunLike.addMonoid
- FunLike.mulAction
- FunLike.coe_intCast
- QuadraticMap.coeFn_smul
- CuspForm.coe_smul
- SlashInvariantForm.coe_smul
- MultilinearMap.coe_smul
- FunLike.addLeftCancelMonoid
- SlashInvariantForm.smul_apply
- SlashInvariantForm.smul_applyℝ
- FunLike.distribMulAction
- SchwartzMap.smul_apply
- NonarchAddGroupSeminorm.smul_apply
- FunLike.ring
- ProbabilityTheory.Kernel.coe_nsmul
- FunLike.addCancelMonoid
- FunLike.subtractionMonoid
- MeasureTheory.VectorMeasure.coe_smul
- ModularForm.smul_apply
- ModularForm.IsGLPos.smul_apply
- GroupSeminorm.coe_smul
- ContinuousMultilinearMap.smul_apply
- FunLike.distribSMul
- UniformConvergenceCLM.smul_apply
- FunLike.smulCommClass
Ancestors0
No ancestors.