Action

📁 Source: Mathlib/Analysis/Normed/Module/Ball/Action.lean

Statistics

Metric	Count
Definitions mulActionClosedBallBall, mulActionClosedBallClosedBall, mulActionSphereBall, mulActionSphereClosedBall, mulActionSphereSphere	5
Theorems continuousSMul_closedBall_ball, continuousSMul_closedBall_closedBall, continuousSMul_sphere_ball, continuousSMul_sphere_closedBall, continuousSMul_sphere_sphere, instSMulCommClass_closedBall_closedBall_ball, instSMulCommClass_closedBall_closedBall_closedBall, instSMulCommClass_sphere_ball_ball, instSMulCommClass_sphere_closedBall_ball, instSMulCommClass_sphere_closedBall_closedBall, instSMulCommClass_sphere_sphere_ball, instSMulCommClass_sphere_sphere_closedBall, instSMulCommClass_sphere_sphere_sphere, isScalarTower_closedBall_ball_ball, isScalarTower_closedBall_closedBall_ball, isScalarTower_closedBall_closedBall_closedBall, isScalarTower_sphere_ball_ball, isScalarTower_sphere_closedBall_ball, isScalarTower_sphere_closedBall_closedBall, isScalarTower_sphere_sphere_ball, isScalarTower_sphere_sphere_closedBall, isScalarTower_sphere_sphere_sphere, ne_neg_of_mem_sphere, ne_neg_of_mem_unit_sphere	24
Total	29

(root)

Definitions

Name	Category	Theorems
mulActionClosedBallBall 📖	CompOp	6 math math: continuousSMul_closedBall_ball, isScalarTower_closedBall_ball_ball, isScalarTower_sphere_closedBall_ball, instSMulCommClass_closedBall_closedBall_ball, instSMulCommClass_sphere_closedBall_ball, isScalarTower_closedBall_closedBall_ball
mulActionClosedBallClosedBall 📖	CompOp	6 math math: isScalarTower_closedBall_closedBall_closedBall, isScalarTower_sphere_closedBall_closedBall, instSMulCommClass_sphere_closedBall_closedBall, continuousSMul_closedBall_closedBall, isScalarTower_closedBall_closedBall_ball, instSMulCommClass_closedBall_closedBall_closedBall
mulActionSphereBall 📖	CompOp	7 math math: continuousSMul_sphere_ball, isScalarTower_sphere_sphere_ball, isScalarTower_sphere_closedBall_ball, instSMulCommClass_sphere_ball_ball, isScalarTower_sphere_ball_ball, instSMulCommClass_sphere_closedBall_ball, instSMulCommClass_sphere_sphere_ball
mulActionSphereClosedBall 📖	CompOp	6 math math: isScalarTower_sphere_closedBall_closedBall, instSMulCommClass_sphere_closedBall_closedBall, continuousSMul_sphere_closedBall, isScalarTower_sphere_sphere_closedBall, isScalarTower_sphere_closedBall_ball, instSMulCommClass_sphere_sphere_closedBall
mulActionSphereSphere 📖	CompOp	5 math math: continuousSMul_sphere_sphere, instSMulCommClass_sphere_sphere_sphere, isScalarTower_sphere_sphere_sphere, isScalarTower_sphere_sphere_closedBall, isScalarTower_sphere_sphere_ball

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul_closedBall_ball 📖	mathematical	—	ContinuousSMul Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	NormedDivisionRing.to_normOneClass Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' Continuous.snd
continuousSMul_closedBall_closedBall 📖	mathematical	—	ContinuousSMul Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallClosedBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	NormedDivisionRing.to_normOneClass Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' Continuous.snd
continuousSMul_sphere_ball 📖	mathematical	—	ContinuousSMul Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' Continuous.snd
continuousSMul_sphere_closedBall 📖	mathematical	—	ContinuousSMul Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereClosedBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' Continuous.snd
continuousSMul_sphere_sphere 📖	mathematical	—	ContinuousSMul Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereSphere instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' Continuous.snd
instSMulCommClass_closedBall_closedBall_ball 📖	mathematical	—	SMulCommClass Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallBall	—	NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
instSMulCommClass_closedBall_closedBall_closedBall 📖	mathematical	—	SMulCommClass Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallClosedBall	—	NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
instSMulCommClass_sphere_ball_ball 📖	mathematical	—	SMulCommClass Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SMulZeroClass.toSMul SemigroupWithZero.toMulZeroClass Metric.unitBall.instSemigroupWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm Algebra.to_smulCommClass
instSMulCommClass_sphere_closedBall_ball 📖	mathematical	—	SMulCommClass Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereBall Metric.unitClosedBall.instMonoid mulActionClosedBallBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
instSMulCommClass_sphere_closedBall_closedBall 📖	mathematical	—	SMulCommClass Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereClosedBall Metric.unitClosedBall.instMonoid mulActionClosedBallClosedBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
instSMulCommClass_sphere_sphere_ball 📖	mathematical	—	SMulCommClass Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
instSMulCommClass_sphere_sphere_closedBall 📖	mathematical	—	SMulCommClass Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereClosedBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
instSMulCommClass_sphere_sphere_sphere 📖	mathematical	—	SMulCommClass Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereSphere	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass SMulCommClass.smul_comm
isScalarTower_closedBall_ball_ball 📖	mathematical	—	IsScalarTower Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SMulZeroClass.toSMul SemigroupWithZero.toMulZeroClass Metric.unitBall.instSemigroupWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero	—	NormedDivisionRing.to_normOneClass smul_assoc IsScalarTower.right
isScalarTower_closedBall_closedBall_ball 📖	mathematical	—	IsScalarTower Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallClosedBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace mulActionClosedBallBall	—	NormedDivisionRing.to_normOneClass smul_assoc
isScalarTower_closedBall_closedBall_closedBall 📖	mathematical	—	IsScalarTower Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitClosedBall.instMonoid NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing MulAction.toSemigroupAction mulActionClosedBallClosedBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace	—	NormedDivisionRing.to_normOneClass smul_assoc
isScalarTower_sphere_ball_ball 📖	mathematical	—	IsScalarTower Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SMulZeroClass.toSMul SemigroupWithZero.toMulZeroClass Metric.unitBall.instSemigroupWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass smul_assoc IsScalarTower.right
isScalarTower_sphere_closedBall_ball 📖	mathematical	—	IsScalarTower Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereClosedBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace Metric.unitClosedBall.instMonoid mulActionClosedBallBall mulActionSphereBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass smul_assoc
isScalarTower_sphere_closedBall_closedBall 📖	mathematical	—	IsScalarTower Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereClosedBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace Metric.unitClosedBall.instMonoid mulActionClosedBallClosedBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass smul_assoc
isScalarTower_sphere_sphere_ball 📖	mathematical	—	IsScalarTower Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereSphere NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace mulActionSphereBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass smul_assoc
isScalarTower_sphere_sphere_closedBall 📖	mathematical	—	IsScalarTower Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereSphere NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace mulActionSphereClosedBall	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass smul_assoc
isScalarTower_sphere_sphere_sphere 📖	mathematical	—	IsScalarTower Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instOne SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SemigroupAction.toSMul Monoid.toSemigroup Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedField.toNormedDivisionRing NormedDivisionRing.to_normOneClass MulAction.toSemigroupAction mulActionSphereSphere NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass smul_assoc
ne_neg_of_mem_sphere 📖	—	—	—	—	IsAddTorsionFree.of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero ne_zero_of_mem_sphere self_eq_neg
ne_neg_of_mem_unit_sphere 📖	—	—	—	—	ne_neg_of_mem_sphere one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing

---

← Back to Index