AddTorsor

📁 Source: Mathlib/Analysis/Normed/Affine/AddTorsor.lean

Statistics

Metric	Count
Definitions `ofMapMidpoint`, `smulTorsor`	2
Theorems `smulTorsor_apply`, `smulTorsor_preimage_ball`, `smulTorsor_ratio`, `smulTorsor_symm_apply`, `antilipschitzWith_lineMap`, `dist_center_homothety`, `dist_homothety_center`, `dist_homothety_self`, `dist_left_lineMap`, `dist_left_midpoint`, `dist_left_midpoint_eq_dist_right_midpoint`, `dist_left_pointReflection`, `dist_lineMap_left`, `dist_lineMap_lineMap`, `dist_lineMap_right`, `dist_midpoint_left`, `dist_midpoint_midpoint_le`, `dist_midpoint_midpoint_le'`, `dist_midpoint_right`, `dist_pointReflection_left`, `dist_pointReflection_right`, `dist_right_lineMap`, `dist_right_midpoint`, `dist_right_pointReflection`, `dist_self_homothety`, `lipschitzWith_lineMap`, `nndist_center_homothety`, `nndist_homothety_center`, `nndist_homothety_self`, `nndist_left_lineMap`, `nndist_left_midpoint`, `nndist_lineMap_left`, `nndist_lineMap_lineMap`, `nndist_lineMap_right`, `nndist_midpoint_left`, `nndist_midpoint_midpoint_le`, `nndist_midpoint_midpoint_le'`, `nndist_midpoint_right`, `nndist_right_lineMap`, `nndist_right_midpoint`, `nndist_self_homothety`	41
Total	43

AffineMap

Definitions

Name	Category	Theorems
`ofMapMidpoint` 📖	CompOp	—

DilationEquiv

Definitions

Name	Category	Theorems
`smulTorsor` 📖	CompOp	4 math math: `smulTorsor_symm_apply`, `smulTorsor_apply`, `smulTorsor_ratio`, `smulTorsor_preimage_ball`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulTorsor_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `EquivLike.toFunLike` `instEquivLike` `smulTorsor` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddTorsor.toAddTorsor` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`smulTorsor_preimage_ball` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `DilationEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `EquivLike.toFunLike` `instEquivLike` `smulTorsor` `Metric.ball` `Norm.norm` `NormedDivisionRing.toNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne`	—	`Set.ext` `dist_vadd_left` `norm_smul` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `dist_zero_right`
`smulTorsor_ratio` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `smulTorsor` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing`	—	`instDilationClassOfDilationEquivClass` `instDilationEquivClass` `Dilation.ratio_unique_of_dist_ne_zero` `dist_vadd_cancel_right` `dist_eq_norm` `norm_smul`
`smulTorsor_symm_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `smulTorsor` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `VSub.vsub` `AddTorsor.toVSub` `NormedAddTorsor.toAddTorsor`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitzWith_lineMap` 📖	mathematical	—	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `NNReal` `NNReal.instInv` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`AntilipschitzWith.of_le_mul_dist` `dist_lineMap_lineMap` `NNReal.coe_inv` `dist_nndist` `mul_left_comm` `inv_mul_cancel₀` `dist_ne_zero` `mul_one` `le_refl`
`dist_center_homothety` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`dist_vadd_right` `norm_smul` `NormedSpace.toNormSMulClass` `dist_comm`
`dist_homothety_center` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`dist_comm` `dist_center_homothety`
`dist_homothety_self` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`AffineMap.homothety_eq_lineMap` `dist_lineMap_right`
`dist_left_lineMap` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`dist_comm` `dist_lineMap_left`
`dist_left_midpoint` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint.eq_1` `dist_comm` `dist_lineMap_left` `invOf_eq_inv` `norm_inv`
`dist_left_midpoint_eq_dist_right_midpoint` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_left_midpoint` `dist_right_midpoint`
`dist_left_pointReflection` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor`	—	`dist_comm` `dist_pointReflection_left`
`dist_lineMap_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`AffineMap.lineMap_apply_zero` `dist_zero_right` `dist_lineMap_lineMap`
`dist_lineMap_lineMap` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `Real` `Real.instMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`dist_comm` `dist_eq_norm_vsub` `vadd_vsub_vadd_cancel_right` `norm_smul` `NormedSpace.toNormSMulClass`
`dist_lineMap_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`AffineMap.lineMap_apply_one` `dist_eq_norm'` `dist_lineMap_lineMap`
`dist_midpoint_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_comm` `dist_left_midpoint`
`dist_midpoint_midpoint_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `midpoint` `Real.instRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `DivisionSemiring.toSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Real.norm_ofNat` `dist_midpoint_midpoint_le'`
`dist_midpoint_midpoint_le'` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_eq_norm_vsub` `midpoint_vsub_midpoint` `midpoint_eq_smul_add` `norm_smul` `NormedSpace.toNormSMulClass` `invOf_eq_inv` `norm_inv` `div_eq_inv_mul` `le_imp_le_of_le_of_le` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_add_le` `norm_nonneg` `le_refl`
`dist_midpoint_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `dist_midpoint_left` `dist_comm`
`dist_pointReflection_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor`	—	`dist_eq_norm_vsub` `Equiv.pointReflection_vsub_left`
`dist_pointReflection_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_eq_norm_vsub` `Equiv.pointReflection_vsub_right` `Nat.cast_smul_eq_nsmul` `norm_smul` `NormedSpace.toNormSMulClass`
`dist_right_lineMap` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`dist_comm` `dist_lineMap_right`
`dist_right_midpoint` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `Real` `Real.instMul` `Real.instInv` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_comm` `dist_midpoint_right`
`dist_right_pointReflection` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_comm` `dist_pointReflection_right`
`dist_self_homothety` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`dist_comm` `dist_homothety_self`
`lipschitzWith_lineMap` 📖	mathematical	—	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`LipschitzWith.of_dist_le_mul` `Eq.le` `dist_lineMap_lineMap` `mul_comm`
`nndist_center_homothety` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`NNReal.eq` `dist_center_homothety`
`nndist_homothety_center` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`NNReal.eq` `dist_homothety_center`
`nndist_homothety_self` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`NNReal.eq` `dist_homothety_self`
`nndist_left_lineMap` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing`	—	`NNReal.eq` `dist_left_lineMap`
`nndist_left_midpoint` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `NNReal.eq` `dist_left_midpoint`
`nndist_lineMap_left` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing`	—	`NNReal.eq` `dist_lineMap_left`
`nndist_lineMap_lineMap` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`NNReal.eq` `dist_lineMap_lineMap`
`nndist_lineMap_right` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NNReal.eq` `dist_lineMap_right`
`nndist_midpoint_left` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `NNReal.eq` `dist_midpoint_left`
`nndist_midpoint_midpoint_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `midpoint` `Real` `Real.instRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `DivisionSemiring.toSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `NNReal.instDiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`dist_midpoint_midpoint_le`
`nndist_midpoint_midpoint_le'` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `NNReal.instDiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_midpoint_midpoint_le'`
`nndist_midpoint_right` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `NNReal.eq` `dist_midpoint_right`
`nndist_right_lineMap` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NNReal.eq` `dist_right_lineMap`
`nndist_right_midpoint` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `midpoint` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `NNReal.eq` `dist_right_midpoint`
`nndist_self_homothety` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.homothety` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`NNReal.eq` `dist_self_homothety`

---

← Back to Index