Theorems · Inductive type · functional analysis
ENormSMulClass
(α : Type u_3) → (β : Type u_4) → [ENorm α] → [ENorm β] → [SMul α β] → Prop
Mixin class for scalar-multiplication actions with a strictly multiplicative norm, i.e.
‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ.
- Defined in
- Mathlib.Analysis.Normed.MulAction
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENormstatement · cited by 155
Cited by20
Results whose statement or proof uses this declaration.
- enorm_smulstatement and proof · cited by 14
- Manifold.riemannianEDist_le_pathELengthstatement and proof · cited by 4
- Manifold.exists_lt_locally_constant_of_riemannianEDist_ltstatement and proof · cited by 3
- Manifold.pathELength_comp_of_monotoneOnstatement and proof · cited by 2
- MeasureTheory.eLpNorm_const_smul_le'statement and proof · cited by 1
- MeasureTheory.Integrable.smul_enormstatement and proof · cited by 1
- ProbabilityTheory.IndepFun.integrable_mulstatement and proof · cited by 1
- ProbabilityTheory.IndepFun.integrable_smulstatement and proof · cited by 1
- MeasureTheory.Integrable.fun_smul_enormstatement · cited by 1
- MeasureTheory.HasFiniteIntegral.smul_enormstatement and proof · cited by 1
- ENormSMulClass.enorm_smulstatement and proof · cited by 1
- Manifold.pathELength_comp_of_antitoneOnstatement and proof · cited by 1