Theorems · Inductive type · functional analysis
NormSMulClass
(α : Type u_3) → (β : Type u_4) → [Norm α] → [Norm β] → [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
- 107 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · 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.
- Normstatement · cited by 512
Cited by112
Results whose statement or proof uses this declaration.
- norm_smulstatement and proof · cited by 242
- MeasureTheory.integral_smulstatement and proof · cited by 23
- nnnorm_smulstatement and proof · cited by 14
- dist_smul₀statement and proof · cited by 11
- intervalIntegral.integral_smulstatement and proof · cited by 10
- Balanced.smul_monostatement and proof · cited by 6
- tendsto_zero_of_isBoundedUnder_smul_of_tendsto_coboundedstatement and proof · cited by 5
- DilationEquiv.smulTorsorstatement and proof · cited by 5
- CircleIntegrable.continuousOn_smulstatement and proof · cited by 4
- Seminorm.convex_ballstatement and proof · cited by 4
- Seminorm.restrictScalarsstatement and proof · cited by 4
- Asymptotics.IsBigO.smulstatement and proof · cited by 4