Structures · Topology
IsIsometricSMul
A multiplicative action is isometric if each map x ↦ c • x is an isometry.
- Shape
- 2 explicit arguments · adds isometry_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- DomMulAct
- Units
- Matrix.SpecialLinearGroup
- Prod
- ULift
- MulOpposite
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by98
- IsIsometricSMul.isometry_smul
- IsometryEquiv.constSMul
- IsometryEquiv.inv
- edist_inv_inv
- IsometryEquiv.divLeft
- dist_mul_left
- dist_mul_right
- IsometryEquiv.mulRight
- Metric.smul_sphere
- Metric.smul_closedBall
- IsometryEquiv.divRight
- Metric.preimage_smul_eball
- IsometryEquiv.mulLeft
- Metric.preimage_smul_closedEBall
- isometry_mul_left
- isometry_mul_right
- dist_smul
- Metric.smul_eball
- nndist_smul
- Metric.preimage_smul_ball
- dist_inv_inv
- Metric.preimage_smul_closedBall
- Metric.smul_closedEBall
- edist_mul_right
- Metric.smul_ball
- edist_mul_left
- IsometryEquiv.divLeft_apply
- IsometryEquiv.constSMul_symm
- Metric.preimage_mul_left_closedEBall
- Metric.preimage_mul_right_ball
- Metric.preimage_mul_left_eball
- nndist_mul_right
- IsometryEquiv.divLeft_symm_apply
- nndist_mul_left
- Metric.infEDist_smul
- nndist_inv_inv
- Bornology.IsBounded.smul
- Metric.preimage_mul_right_closedEBall
- Metric.preimage_mul_right_eball
- isometry_inv
- Prod.isIsometricSMul''
- IsometryEquiv.mulLeft_toEquiv
- Additive.isIsIsometricVAdd'
- MeasureTheory.instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul
- Pi.isIsometricSMul''
- IsometryEquiv.mulRight_toEquiv
- nndist_div_right
- dist_div_right
- EMetric.preimage_mul_left_closedBall
- Prod.instIsIsometricSMul
Ancestors0
No ancestors.