Structures · Analysis
ENormSMulClass
Mixin class for scalar-multiplication actions with a strictly multiplicative norm, i.e.
‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ.
- Defined in
- Mathlib.Analysis.Normed.MulAction
- Shape
- 2 explicit arguments · adds enorm_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- enorm_smul
- Manifold.riemannianEDist_le_pathELength
- Manifold.exists_lt_locally_constant_of_riemannianEDist_lt
- Manifold.pathELength_comp_of_monotoneOn
- MeasureTheory.HasFiniteIntegral.smul_enorm
- MeasureTheory.Integrable.fun_smul_enorm
- MeasureTheory.Integrable.smul_enorm
- ProbabilityTheory.IndepFun.integrable_smul
- ENormSMulClass.enorm_smul
- Manifold.pathELength_comp_of_antitoneOn
- MeasureTheory.eLpNorm_const_smul_le'
- ProbabilityTheory.IndepFun.integrable_mul
- Manifold.riemannianEDist_triangle
- MeasureTheory.MemLp.const_smul'
- Manifold.riemannianEDist_comm
- MeasureTheory.eLpNorm'_const_smul_le'
- Manifold.riemannianEDist_self
- MeasureTheory.eLpNormEssSup_const_smul_le'
Ancestors0
No ancestors.