RightAngle

📁 Source: Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean

Statistics

Metric	Count
Definitions	0
Theorems `angle_eq_arccos_of_angle_eq_pi_div_two`, `angle_eq_arcsin_of_angle_eq_pi_div_two`, `angle_eq_arctan_of_angle_eq_pi_div_two`, `angle_le_pi_div_two_of_angle_eq_pi_div_two`, `angle_lt_pi_div_two_of_angle_eq_pi_div_two`, `angle_pos_of_angle_eq_pi_div_two`, `cos_angle_mul_dist_of_angle_eq_pi_div_two`, `cos_angle_of_angle_eq_pi_div_two`, `dist_div_cos_angle_of_angle_eq_pi_div_two`, `dist_div_sin_angle_of_angle_eq_pi_div_two`, `dist_div_tan_angle_of_angle_eq_pi_div_two`, `dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two`, `sin_angle_mul_dist_of_angle_eq_pi_div_two`, `sin_angle_of_angle_eq_pi_div_two`, `tan_angle_mul_dist_of_angle_eq_pi_div_two`, `tan_angle_of_angle_eq_pi_div_two`, `angle_add_eq_arccos_of_inner_eq_zero`, `angle_add_eq_arcsin_of_inner_eq_zero`, `angle_add_eq_arctan_of_inner_eq_zero`, `angle_add_le_pi_div_two_of_inner_eq_zero`, `angle_add_lt_pi_div_two_of_inner_eq_zero`, `angle_add_pos_of_inner_eq_zero`, `angle_sub_eq_arccos_of_inner_eq_zero`, `angle_sub_eq_arcsin_of_inner_eq_zero`, `angle_sub_eq_arctan_of_inner_eq_zero`, `angle_sub_le_pi_div_two_of_inner_eq_zero`, `angle_sub_lt_pi_div_two_of_inner_eq_zero`, `angle_sub_pos_of_inner_eq_zero`, `cos_angle_add_mul_norm_of_inner_eq_zero`, `cos_angle_add_of_inner_eq_zero`, `cos_angle_sub_mul_norm_of_inner_eq_zero`, `cos_angle_sub_of_inner_eq_zero`, `norm_add_sq_eq_norm_sq_add_norm_sq'`, `norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two`, `norm_div_cos_angle_add_of_inner_eq_zero`, `norm_div_cos_angle_sub_of_inner_eq_zero`, `norm_div_sin_angle_add_of_inner_eq_zero`, `norm_div_sin_angle_sub_of_inner_eq_zero`, `norm_div_tan_angle_add_of_inner_eq_zero`, `norm_div_tan_angle_sub_of_inner_eq_zero`, `norm_sub_sq_eq_norm_sq_add_norm_sq'`, `norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two`, `sin_angle_add_mul_norm_of_inner_eq_zero`, `sin_angle_add_of_inner_eq_zero`, `sin_angle_sub_mul_norm_of_inner_eq_zero`, `sin_angle_sub_of_inner_eq_zero`, `tan_angle_add_mul_norm_of_inner_eq_zero`, `tan_angle_add_of_inner_eq_zero`, `tan_angle_sub_mul_norm_of_inner_eq_zero`, `tan_angle_sub_of_inner_eq_zero`	50
Total	50

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angle_eq_arccos_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arccos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub'` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`
`angle_eq_arcsin_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arcsin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_ne_zero`
`angle_eq_arctan_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arctan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `dist_eq_norm_vsub'` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_ne_zero`
`angle_le_pi_div_two_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instLE`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`
`angle_lt_pi_div_two_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instLT`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_ne_zero`
`angle_pos_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instLT` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.angle_add_pos_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_eq_zero_iff_eq` `vsub_ne_zero`
`cos_angle_mul_dist_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.cos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub'` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`
`cos_angle_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.cos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub'` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.cos_angle_add_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`
`dist_div_cos_angle_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.cos`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub'` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_eq_zero_iff_eq` `vsub_ne_zero`
`dist_div_sin_angle_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.sin`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_eq_zero_iff_eq` `vsub_ne_zero`
`dist_div_tan_angle_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.tan`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `dist_eq_norm_vsub'` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_eq_zero_iff_eq` `vsub_ne_zero`
`dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two` 📖	mathematical	—	`Real` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.instAdd` `angle` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_comm` `dist_eq_norm_vsub` `InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two` `vsub_sub_vsub_cancel_right` `neg_vsub_eq_vsub_rev` `norm_neg`
`sin_angle_mul_dist_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.sin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`
`sin_angle_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.sin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.sin_angle_add_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_ne_zero`
`tan_angle_mul_dist_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.tan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `dist_eq_norm_vsub'` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two` `vsub_eq_zero_iff_eq` `vsub_ne_zero`
`tan_angle_of_angle_eq_pi_div_two` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.tan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `angle.eq_1` `dist_eq_norm_vsub` `dist_eq_norm_vsub'` `vsub_add_vsub_cancel` `add_comm` `InnerProductGeometry.tan_angle_add_of_inner_eq_zero` `neg_vsub_eq_vsub_rev` `inner_neg_left` `neg_eq_zero` `real_inner_comm` `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`

InnerProductGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angle_add_eq_arccos_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arccos` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`angle.eq_1` `inner_add_right` `add_zero` `real_inner_self_eq_norm_mul_norm` `Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `div_zero` `Real.arccos_zero` `zero_div` `div_mul_eq_div_div` `mul_self_div_self`
`angle_add_eq_arcsin_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arcsin` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`pow_two` `norm_add_sq_eq_norm_sq_add_norm_sq_real` `ne_of_lt` `Left.add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `norm_ne_zero_iff` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Left.add_pos_of_nonneg_of_pos` `angle_add_eq_arccos_of_inner_eq_zero` `Real.arccos_eq_arcsin` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `norm_nonneg` `div_pow` `one_sub_div` `add_sub_cancel_left` `Real.sqrt_sq`
`angle_add_eq_arctan_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arctan` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`angle_add_eq_arcsin_of_inner_eq_zero` `Real.arctan_eq_arcsin` `div_mul_eq_div_div` `norm_add_eq_sqrt_iff_real_inner_eq_zero` `Real.sqrt_sq` `norm_nonneg` `Nat.cast_one` `Real.sqrt_mul` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_pow` `pow_two` `mul_add` `Distrib.leftDistribClass` `mul_one` `mul_div` `mul_comm` `div_self` `LT.lt.ne'` `mul_self_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `norm_ne_zero_iff`
`angle_add_le_pi_div_two_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instLE` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `angle_add_eq_arccos_of_inner_eq_zero` `Real.arccos_le_pi_div_two` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg`
`angle_add_lt_pi_div_two_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instLT` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `angle_add_eq_arccos_of_inner_eq_zero` `Real.arccos_lt_pi_div_two` `norm_add_eq_sqrt_iff_real_inner_eq_zero` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `Real.sqrt_pos` `Left.add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `norm_ne_zero_iff` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`angle_add_pos_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Real.instLT` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`angle_add_eq_arccos_of_inner_eq_zero` `Real.arccos_pos` `norm_add_eq_sqrt_iff_real_inner_eq_zero` `norm_zero` `MulZeroClass.mul_zero` `zero_add` `Real.sqrt_mul_self` `zero_div` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.sqrt_pos` `Left.add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `norm_ne_zero_iff` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Real.lt_sqrt` `norm_nonneg` `pow_two`
`angle_sub_eq_arccos_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arccos` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `angle_add_eq_arccos_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero`
`angle_sub_eq_arcsin_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arcsin` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `angle_add_eq_arcsin_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `neg_ne_zero` `norm_neg`
`angle_sub_eq_arctan_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arctan` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `angle_add_eq_arctan_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `norm_neg`
`angle_sub_le_pi_div_two_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instLE` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `angle_add_le_pi_div_two_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero`
`angle_sub_lt_pi_div_two_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instLT` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `angle_add_lt_pi_div_two_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero`
`angle_sub_pos_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Real.instLT` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `angle_add_pos_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `neg_ne_zero`
`cos_angle_add_mul_norm_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instMul` `Real.cos` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`cos_angle_add_of_inner_eq_zero` `norm_add_sq_eq_norm_sq_add_norm_sq_real` `mul_self_eq_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `add_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `MulZeroClass.zero_mul` `zero_div` `div_mul_cancel₀`
`cos_angle_add_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.cos` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`angle_add_eq_arccos_of_inner_eq_zero` `Real.cos_arccos` `le_trans` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_self_le_mul_self_iff` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_add_sq_eq_norm_sq_add_norm_sq_real` `le_add_of_nonneg_right` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono`
`cos_angle_sub_mul_norm_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instMul` `Real.cos` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `cos_angle_add_mul_norm_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero`
`cos_angle_sub_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.cos` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `cos_angle_add_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero`
`norm_add_sq_eq_norm_sq_add_norm_sq'` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two`
`norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two` 📖	mathematical	—	`Real` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAdd` `angle` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero` `inner_eq_zero_iff_angle_eq_pi_div_two`
`norm_div_cos_angle_add_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.cos` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`cos_angle_add_of_inner_eq_zero` `div_div_eq_mul_div` `mul_comm` `div_eq_mul_inv` `mul_inv_cancel_right₀` `norm_ne_zero_iff` `add_zero` `div_div_self`
`norm_div_cos_angle_sub_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.cos` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `norm_div_cos_angle_add_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero`
`norm_div_sin_angle_add_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.sin` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `zero_add` `angle_zero_left` `Real.sin_pi_div_two` `div_one` `sin_angle_add_of_inner_eq_zero` `div_div_eq_mul_div` `mul_comm` `div_eq_mul_inv` `mul_inv_cancel_right₀` `norm_ne_zero_iff`
`norm_div_sin_angle_sub_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.sin` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `norm_neg` `norm_div_sin_angle_add_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `neg_ne_zero`
`norm_div_tan_angle_add_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.tan` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`tan_angle_add_of_inner_eq_zero` `norm_zero` `div_zero` `div_div_eq_mul_div` `mul_comm` `div_eq_mul_inv` `mul_inv_cancel_right₀` `norm_ne_zero_iff`
`norm_div_tan_angle_sub_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.tan` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `norm_neg` `norm_div_tan_angle_add_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `neg_ne_zero`
`norm_sub_sq_eq_norm_sq_add_norm_sq'` 📖	mathematical	`angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two`
`norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two` 📖	mathematical	—	`Real` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instAdd` `angle` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero` `inner_eq_zero_iff_angle_eq_pi_div_two`
`sin_angle_add_mul_norm_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instMul` `Real.sin` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Nat.instAtLeastTwoHAddOfNat` `add_zero` `angle_zero_right` `Real.sin_pi_div_two` `norm_zero` `MulZeroClass.mul_zero` `sin_angle_add_of_inner_eq_zero` `not_and_or` `div_mul_cancel₀` `mul_self_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `norm_add_sq_eq_norm_sq_add_norm_sq_real` `ne_of_lt` `Left.add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `norm_ne_zero_iff` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Left.add_pos_of_nonneg_of_pos`
`sin_angle_add_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.sin` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`angle_add_eq_arcsin_of_inner_eq_zero` `Real.sin_arcsin` `le_trans` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_self_le_mul_self_iff` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_add_sq_eq_norm_sq_add_norm_sq_real` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono`
`sin_angle_sub_mul_norm_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.instMul` `Real.sin` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `sin_angle_add_mul_norm_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `norm_neg`
`sin_angle_sub_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.sin` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `sin_angle_add_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `neg_ne_zero` `norm_neg`
`tan_angle_add_mul_norm_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Real.instMul` `Real.tan` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`tan_angle_add_of_inner_eq_zero` `IsUnit.div_mul_cancel` `norm_zero` `zero_div` `MulZeroClass.zero_mul`
`tan_angle_add_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.tan` `angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Nat.instAtLeastTwoHAddOfNat` `zero_add` `angle_zero_left` `Real.tan_pi_div_two` `norm_zero` `div_zero` `angle_add_eq_arctan_of_inner_eq_zero` `Real.tan_arctan`
`tan_angle_sub_mul_norm_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Real.instMul` `Real.tan` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `tan_angle_add_mul_norm_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `norm_neg`
`tan_angle_sub_of_inner_eq_zero` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero`	`Real.tan` `angle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sub_eq_add_neg` `tan_angle_add_of_inner_eq_zero` `inner_neg_right` `neg_eq_zero` `norm_neg`

---

← Back to Index