Midpoint

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean

Statistics

Metric	Count
Definitions `ofMapMidpoint`, `midpoint`	2
Theorems `coe_ofMapMidpoint`, `map_midpoint`, `midpoint_pointReflection_left`, `midpoint_pointReflection_right`, `pointReflection_midpoint_left`, `pointReflection_midpoint_right`, `map_midpoint`, `pointReflection_midpoint_left`, `pointReflection_midpoint_right`, `left_eq_midpoint_iff`, `left_sub_midpoint`, `left_vsub_midpoint`, `midpoint_add_self`, `midpoint_add_sub`, `midpoint_comm`, `midpoint_eq_iff`, `midpoint_eq_iff'`, `midpoint_eq_left_iff`, `midpoint_eq_midpoint_iff_vsub_eq_vsub`, `midpoint_eq_right_iff`, `midpoint_eq_smul_add`, `midpoint_neg_self`, `midpoint_pointReflection_left`, `midpoint_pointReflection_right`, `midpoint_self`, `midpoint_self_neg`, `midpoint_sub_add`, `midpoint_sub_left`, `midpoint_sub_right`, `midpoint_unique`, `midpoint_vadd_midpoint`, `midpoint_vsub`, `midpoint_vsub_left`, `midpoint_vsub_midpoint`, `midpoint_vsub_midpoint_same_left`, `midpoint_vsub_midpoint_same_right`, `midpoint_vsub_right`, `midpoint_zero_add`, `right_eq_midpoint_iff`, `right_sub_midpoint`, `right_vsub_midpoint`, `vsub_midpoint`	42
Total	44

AddMonoidHom

Definitions

Name	Category	Theorems
`ofMapMidpoint` 📖	CompOp	1 math math: `coe_ofMapMidpoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofMapMidpoint` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `ofMapMidpoint`	—	`Nat.instAtLeastTwoHAddOfNat`

AffineEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_midpoint` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `apply_lineMap`
`midpoint_pointReflection_left` 📖	mathematical	—	`midpoint` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_pointReflection_left`
`midpoint_pointReflection_right` 📖	mathematical	—	`midpoint` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_pointReflection_right`
`pointReflection_midpoint_left` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection` `midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint.eq_1` `pointReflection_apply` `AffineMap.lineMap_apply` `vadd_vsub` `vadd_vadd` `add_smul` `two_mul` `mul_invOf_self` `one_smul` `vsub_vadd`
`pointReflection_midpoint_right` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection` `midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `pointReflection_midpoint_left`

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_midpoint` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `instFunLike` `midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `apply_lineMap`

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pointReflection_midpoint_left` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `pointReflection` `AddCommGroup.toAddGroup` `midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint.eq_1` `pointReflection_apply` `AffineMap.lineMap_apply` `vadd_vsub` `vadd_vadd` `add_smul` `two_mul` `mul_invOf_self` `one_smul` `vsub_vadd`
`pointReflection_midpoint_right` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `pointReflection` `AddCommGroup.toAddGroup` `midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `pointReflection_midpoint_left`

(root)

Definitions

Name	Category	Theorems
`midpoint` 📖	CompOp	97 math math: `vsub_midpoint`, `dist_midpoint_right`, `EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center`, `AffineSubspace.mem_perpBisector_iff_inner_eq_zero'`, `midpoint_add_self`, `dist_left_midpoint`, `midpoint_eq_right_iff`, `sbtw_midpoint_of_ne`, `nndist_midpoint_right`, `lineMap_inv_two`, `IsometryEquiv.midpoint_fixed`, `AffineIsometryEquiv.pointReflection_midpoint_left`, `EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint`, `EuclideanGeometry.oangle_midpoint_right`, `AffineSubspace.mem_perpBisector_iff_inner_eq_zero`, `midpoint_pointReflection_left`, `dist_left_midpoint_eq_dist_right_midpoint`, `Equiv.pointReflection_midpoint_right`, `midpoint_eq_smul_add`, `midpoint_sub_right`, `EuclideanGeometry.oangle_midpoint_rev_left`, `EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center`, `midpoint_le_right`, `midpoint_eq_left_iff`, `dist_midpoint_midpoint_le`, `midpoint_le_midpoint`, `midpoint_comm`, `midpoint_pointReflection_right`, `dist_right_midpoint`, `AffineEquiv.map_midpoint`, `midpoint_self`, `IsometryEquiv.map_midpoint`, `nndist_left_midpoint`, `Affine.Triangle.circumsphere_eq_of_dist_of_oangle`, `Filter.Tendsto.midpoint`, `EuclideanGeometry.oangle_midpoint_left`, `nndist_midpoint_left`, `midpoint_add_sub`, `midpoint_neg_self`, `nndist_midpoint_midpoint_le'`, `midpoint_le_left`, `midpoint_sub_add`, `EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center`, `midpoint_vsub_left`, `Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter`, `midpoint_vadd_midpoint`, `midpoint_eq_iff'`, `Convex.midpoint_mem`, `AffineMap.map_midpoint`, `AffineEquiv.pointReflection_midpoint_right`, `homothety_invOf_two`, `midpoint_vsub_midpoint`, `right_eq_midpoint_iff`, `midpoint_vsub_right`, `pi_midpoint_apply`, `AffineSubspace.midpoint_mem_perpBisector`, `nndist_midpoint_midpoint_le`, `EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq`, `Affine.Triangle.eulerPoint_eq_midpoint`, `midpoint_eq_iff`, `Affine.Simplex.midpoint_faceOppositeCentroid_eulerPoint`, `EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center`, `EuclideanGeometry.oangle_midpoint_rev_right`, `lineMap_one_half`, `EuclideanGeometry.angle_midpoint_eq_pi`, `AffineEquiv.midpoint_pointReflection_left`, `left_le_midpoint`, `midpoint_mem_segment`, `midpoint_unique`, `midpoint_sub_left`, `midpoint_vsub`, `Equiv.pointReflection_midpoint_left`, `EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq`, `dist_midpoint_midpoint_le'`, `right_le_midpoint`, `right_sub_midpoint`, `EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq`, `AffineEquiv.pointReflection_midpoint_left`, `homothety_inv_two`, `dist_midpoint_left`, `midpoint_vsub_midpoint_same_left`, `right_vsub_midpoint`, `nndist_right_midpoint`, `midpoint_eq_midpoint_iff_vsub_eq_vsub`, `EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center`, `wbtw_midpoint`, `eq_midpoint_of_dist_eq_half`, `midpoint_zero_add`, `midpoint_self_neg`, `homothety_one_half`, `left_eq_midpoint_iff`, `left_sub_midpoint`, `midpoint_vsub_midpoint_same_right`, `AffineIsometryEquiv.pointReflection_midpoint_right`, `left_vsub_midpoint`, `Urysohns.CU.lim_eq_midpoint`, `AffineEquiv.midpoint_pointReflection_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_eq_midpoint_iff` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_left_iff`
`left_sub_midpoint` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `midpoint` `addGroupIsAddTorsor` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `left_vsub_midpoint`
`left_vsub_midpoint` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `AffineMap.left_vsub_lineMap`
`midpoint_add_self` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `midpoint_vadd_midpoint` `vadd_eq_add` `add_comm` `midpoint_self`
`midpoint_add_sub` 📖	mathematical	—	`midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `midpoint_sub_add`
`midpoint_comm` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint.eq_1` `AffineMap.lineMap_apply_one_sub` `one_sub_invOf_two`
`midpoint_eq_iff` 📖	mathematical	—	`midpoint` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.pointReflection`	—	`Nat.instAtLeastTwoHAddOfNat` `AffineEquiv.injective_pointReflection_left_of_module` `AffineEquiv.pointReflection_midpoint_left`
`midpoint_eq_iff'` 📖	mathematical	—	`midpoint` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `AddCommGroup.toAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_iff`
`midpoint_eq_left_iff` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_iff` `AffineEquiv.pointReflection_self`
`midpoint_eq_midpoint_iff_vsub_eq_vsub` 📖	mathematical	—	`midpoint` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `vsub_eq_zero_iff_eq` `midpoint_vsub_midpoint` `midpoint_eq_iff` `AffineEquiv.pointReflection_apply` `vsub_eq_sub` `zero_sub` `vadd_eq_add` `add_zero` `neg_eq_iff_eq_neg` `neg_vsub_eq_vsub_rev`
`midpoint_eq_right_iff` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `midpoint_eq_left_iff`
`midpoint_eq_smul_add` 📖	mathematical	—	`midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_iff` `AffineEquiv.pointReflection_apply` `vsub_eq_sub` `vadd_eq_add` `sub_add_eq_add_sub` `two_smul` `smul_smul` `mul_invOf_self` `one_smul` `add_sub_cancel_left`
`midpoint_neg_self` 📖	mathematical	—	`midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NegZeroClass.toZero`	—	`Nat.instAtLeastTwoHAddOfNat` `neg_neg` `midpoint_self_neg`
`midpoint_pointReflection_left` 📖	mathematical	—	`midpoint` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `AddCommGroup.toAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_iff` `Equiv.pointReflection_involutive`
`midpoint_pointReflection_right` 📖	mathematical	—	`midpoint` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.pointReflection` `AddCommGroup.toAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_iff`
`midpoint_self` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `AffineMap.lineMap_same_apply`
`midpoint_self_neg` 📖	mathematical	—	`midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NegZeroClass.toZero`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_smul_add` `add_neg_cancel` `smul_zero`
`midpoint_sub_add` 📖	mathematical	—	`midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `vadd_eq_add` `midpoint_vadd_midpoint` `midpoint_self` `midpoint_neg_self` `add_zero`
`midpoint_sub_left` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `midpoint` `addGroupIsAddTorsor` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_vsub_left`
`midpoint_sub_right` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `midpoint` `addGroupIsAddTorsor` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_vsub_right`
`midpoint_unique` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_iff'`
`midpoint_vadd_midpoint` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `midpoint` `addGroupIsAddTorsor`	—	`Nat.instAtLeastTwoHAddOfNat` `AffineMap.lineMap_vadd_lineMap`
`midpoint_vsub` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `vsub_sub_vsub_cancel_right` `smul_sub` `sub_eq_add_neg` `smul_neg` `neg_vsub_eq_vsub_rev` `add_assoc` `invOf_two_smul_add_invOf_two_smul` `vadd_vsub_assoc` `midpoint_comm` `midpoint.eq_1` `AffineMap.lineMap_apply`
`midpoint_vsub_left` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `AffineMap.lineMap_vsub_left`
`midpoint_vsub_midpoint` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `addGroupIsAddTorsor`	—	`Nat.instAtLeastTwoHAddOfNat` `AffineMap.lineMap_vsub_lineMap`
`midpoint_vsub_midpoint_same_left` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_vsub_midpoint` `vsub_self` `midpoint_eq_smul_add` `zero_add`
`midpoint_vsub_midpoint_same_right` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_vsub_midpoint` `vsub_self` `midpoint_eq_smul_add` `add_zero`
`midpoint_vsub_right` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `midpoint_vsub_left`
`midpoint_zero_add` 📖	mathematical	—	`midpoint` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_midpoint_iff_vsub_eq_vsub` `zero_sub` `sub_add_cancel_right`
`right_eq_midpoint_iff` 📖	mathematical	—	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_eq_right_iff`
`right_sub_midpoint` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `midpoint` `addGroupIsAddTorsor` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `right_vsub_midpoint`
`right_vsub_midpoint` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `midpoint_comm` `left_vsub_midpoint`
`vsub_midpoint` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `midpoint` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `neg_vsub_eq_vsub_rev` `midpoint_vsub` `neg_add` `smul_neg`

---

← Back to Index