MulAction

📁 Source: Mathlib/Analysis/Normed/MulAction.lean

Statistics

Metric	Count
Definitions ENormSMulClass, NormSMulClass	2
Theorems enorm_smul, of_enorm_smul_le, of_nnnorm_smul_le, of_norm_smul_le, isBoundedSMul, isBoundedSMulOpposite, toNormSMulClass, toNormSMulClass_op, norm_smul, of_nnnorm_smul, toIsBoundedSMul, toNormSMulClass, instNormSMulClass, instNormSMulClass, instNormSMulClass, dist_smul_le, dist_smul₀, edist_smul_le, edist_smul₀, enorm_smul, enorm_smul_le, instENormSMulClass, lipschitzWith_smul, nndist_smul_le, nndist_smul₀, nnnorm_smul, nnnorm_smul_le, norm_smul, norm_smul_le	29
Total	31

ENormSMulClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_smul 📖	mathematical	—	ENorm.enorm ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	—

IsBoundedSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_enorm_smul_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	IsBoundedSMul SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	of_norm_smul_le
of_nnnorm_smul_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	IsBoundedSMul SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	of_norm_smul_le
of_norm_smul_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instMul SeminormedRing.toNorm	IsBoundedSMul SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	dist_eq_norm sub_zero smul_sub sub_smul

NonUnitalSeminormedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedSMul 📖	mathematical	—	IsBoundedSMul toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing toNonUnitalRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup toSeminormedAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul	—	dist_eq_norm sub_zero mul_sub norm_mul_le sub_mul
isBoundedSMulOpposite 📖	mathematical	—	IsBoundedSMul MulOpposite MulOpposite.instPseudoMetricSpace toPseudoMetricSpace MulOpposite.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing toNonUnitalRing SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toOppositeSMulWithZero	—	dist_eq_norm sub_zero mul_comm sub_mul norm_mul_le mul_sub

NormMulClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNormSMulClass 📖	mathematical	—	NormSMulClass	—	norm_mul
toNormSMulClass_op 📖	mathematical	—	NormSMulClass MulOpposite SeminormedRing.toNorm MulOpposite.instSeminormedRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SeminormedRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toOppositeModule	—	norm_mul mul_comm

NormSMulClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_smul 📖	mathematical	—	Norm.norm Real Real.instMul	—	—
of_nnnorm_smul 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	NormSMulClass SeminormedRing.toNorm SeminormedAddGroup.toNorm	—	—
toIsBoundedSMul 📖	mathematical	—	IsBoundedSMul SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	IsBoundedSMul.of_norm_smul_le Eq.le norm_smul

NormedDivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNormSMulClass 📖	mathematical	—	NormSMulClass toNorm SeminormedAddGroup.toNorm SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring toDivisionRing MulActionWithZero.toSMulWithZero	—	zero_smul norm_zero MulZeroClass.zero_mul le_antisymm norm_smul_le inv_smul_smul₀ mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt norm_pos_iff norm_inv mul_assoc mul_inv_cancel₀ norm_eq_zero one_mul

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormSMulClass 📖	mathematical	NormSMulClass SeminormedRing.toNorm SeminormedAddGroup.toNorm	seminormedAddGroup instSMul	—	nnnorm_def nnnorm_smul NNReal.mul_finset_sup

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormSMulClass 📖	mathematical	—	NormSMulClass SeminormedRing.toNorm toNorm SeminormedAddGroup.toNorm instSMul	—	nnnorm_smul NNReal.mul_sup

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormSMulClass 📖	mathematical	—	NormSMulClass SeminormedRing.toNorm norm SeminormedAddGroup.toNorm smul	—	norm_smul

(root)

Definitions

Name	Category	Theorems
ENormSMulClass 📖	CompData	1 math math: instENormSMulClass
NormSMulClass 📖	CompData	13 math math: NormMulClass.toNormSMulClass_op, NormedSpace.toNormSMulClass, NormSMulClass.of_nnnorm_smul, Matrix.linftyOpNormSMulClass, WithLp.normSMulClassSeminormedAddCommGroupToProd, Prod.instNormSMulClass, WithLp.instProdNormSMulClass, Matrix.normSMulClass, NormedDivisionRing.toNormSMulClass, Matrix.frobeniusNormSMulClass, RCLike.instNormSMulClassInt, ULift.instNormSMulClass, NormMulClass.toNormSMulClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_smul_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real.instMul Norm.norm SeminormedAddGroup.toNorm	—	dist_eq_norm sub_zero dist_smul_pair
dist_smul₀ 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real Real.instMul Norm.norm SeminormedRing.toNorm	—	dist_eq_norm norm_smul smul_sub
edist_smul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	lipschitzWith_smul
edist_smul₀ 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNNorm.nnnorm SeminormedAddGroup.toNNNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	—	edist_nndist nndist_smul₀
enorm_smul 📖	mathematical	—	ENorm.enorm ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	ENormSMulClass.enorm_smul
enorm_smul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	nnnorm_smul_le
instENormSMulClass 📖	mathematical	—	ENormSMulClass NNNorm.toENorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	—	nnnorm_smul
lipschitzWith_smul 📖	mathematical	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	lipschitzWith_iff_dist_le_mul dist_smul_le
nndist_smul_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddGroup.toPseudoMetricSpace SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	dist_smul_le
nndist_smul₀ 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist SeminormedAddCommGroup.toPseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	—	NNReal.eq dist_smul₀
nnnorm_smul 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing	—	NNReal.eq norm_smul
nnnorm_smul_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	norm_smul_le
norm_smul 📖	mathematical	—	Norm.norm Real Real.instMul	—	NormSMulClass.norm_smul
norm_smul_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real.instMul	—	smul_zero dist_zero dist_zero_right dist_smul_pair

---

← Back to Index