Action

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

Statistics

Metric	Count
Definitions instSMulElemClosedBallOfNatReal, instSMulElemClosedBallOfNatRealBall, instSMulElemSphereOfNatReal, instSMulElemSphereOfNatRealBall, instSMulElemSphereOfNatRealClosedBall, mulActionClosedBallBall, mulActionClosedBallClosedBall, mulActionSphereBall, mulActionSphereClosedBall, mulActionSphereSphere	10
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	34

(root)

Definitions

Name	Category	Theorems
instSMulElemClosedBallOfNatReal 📖	CompOp	7 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, Complex.UnitDisc.instIsScalarTower_closedBall_closedBall
instSMulElemClosedBallOfNatRealBall 📖	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
instSMulElemSphereOfNatReal 📖	CompOp	5 math math: continuousSMul_sphere_sphere, instSMulCommClass_sphere_sphere_sphere, isScalarTower_sphere_sphere_sphere, isScalarTower_sphere_sphere_closedBall, isScalarTower_sphere_sphere_ball
instSMulElemSphereOfNatRealBall 📖	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
instSMulElemSphereOfNatRealClosedBall 📖	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
mulActionClosedBallBall 📖	CompOp	—
mulActionClosedBallClosedBall 📖	CompOp	—
mulActionSphereBall 📖	CompOp	—
mulActionSphereClosedBall 📖	CompOp	—
mulActionSphereSphere 📖	CompOp	—

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 instSMulElemClosedBallOfNatRealBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	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 instSMulElemClosedBallOfNatReal instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	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 instSMulElemSphereOfNatRealBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	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 instSMulElemSphereOfNatRealClosedBall instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	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 instSMulElemSphereOfNatReal instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	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 instSMulElemClosedBallOfNatRealBall	—	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 instSMulElemClosedBallOfNatReal	—	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 instSMulElemSphereOfNatRealBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SMulZeroClass.toSMul SemigroupWithZero.toMulZeroClass Metric.unitBall.instSemigroupWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero	—	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 instSMulElemSphereOfNatRealBall instSMulElemClosedBallOfNatRealBall	—	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 instSMulElemSphereOfNatRealClosedBall instSMulElemClosedBallOfNatReal	—	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 instSMulElemSphereOfNatRealBall	—	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 instSMulElemSphereOfNatRealClosedBall	—	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 instSMulElemSphereOfNatReal	—	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 instSMulElemClosedBallOfNatRealBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SMulZeroClass.toSMul SemigroupWithZero.toMulZeroClass Metric.unitBall.instSemigroupWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero	—	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 instSMulElemClosedBallOfNatReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace instSMulElemClosedBallOfNatRealBall	—	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 instSMulElemClosedBallOfNatReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace	—	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 instSMulElemSphereOfNatRealBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SMulZeroClass.toSMul SemigroupWithZero.toMulZeroClass Metric.unitBall.instSemigroupWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero	—	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 instSMulElemSphereOfNatRealClosedBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace instSMulElemClosedBallOfNatRealBall instSMulElemSphereOfNatRealBall	—	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 instSMulElemSphereOfNatRealClosedBall NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace instSMulElemClosedBallOfNatReal	—	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 instSMulElemSphereOfNatReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace instSMulElemSphereOfNatRealBall	—	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 instSMulElemSphereOfNatReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace instSMulElemSphereOfNatRealClosedBall	—	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 instSMulElemSphereOfNatReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace	—	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