RightAngle

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

Statistics

Metric	Count
Definitions	0
Theorems `abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two`, `cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two`, `cos_oangle_left_of_oangle_eq_pi_div_two`, `cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two`, `cos_oangle_right_of_oangle_eq_pi_div_two`, `dist_div_cos_oangle_left_of_oangle_eq_pi_div_two`, `dist_div_cos_oangle_right_of_oangle_eq_pi_div_two`, `dist_div_sin_oangle_left_of_oangle_eq_pi_div_two`, `dist_div_sin_oangle_right_of_oangle_eq_pi_div_two`, `dist_div_tan_oangle_left_of_oangle_eq_pi_div_two`, `dist_div_tan_oangle_right_of_oangle_eq_pi_div_two`, `oangle_eq_oangle_of_two_zsmul_eq_of_angle_eq_pi_div_two`, `oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two`, `oangle_left_eq_arccos_of_oangle_eq_pi_div_two`, `oangle_left_eq_arcsin_of_oangle_eq_pi_div_two`, `oangle_left_eq_arctan_of_oangle_eq_pi_div_two`, `oangle_right_eq_arccos_of_oangle_eq_pi_div_two`, `oangle_right_eq_arcsin_of_oangle_eq_pi_div_two`, `oangle_right_eq_arctan_of_oangle_eq_pi_div_two`, `sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two`, `sin_oangle_left_of_oangle_eq_pi_div_two`, `sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two`, `sin_oangle_right_of_oangle_eq_pi_div_two`, `tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two`, `tan_oangle_left_of_oangle_eq_pi_div_two`, `tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two`, `tan_oangle_right_of_oangle_eq_pi_div_two`, `cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two`, `cos_oangle_add_left_of_oangle_eq_pi_div_two`, `cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two`, `cos_oangle_add_right_of_oangle_eq_pi_div_two`, `cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two`, `cos_oangle_sub_left_of_oangle_eq_pi_div_two`, `cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two`, `cos_oangle_sub_right_of_oangle_eq_pi_div_two`, `norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two`, `norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two`, `norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two`, `norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two`, `norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two`, `norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two`, `norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two`, `norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two`, `norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two`, `norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two`, `norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two`, `norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two`, `oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two`, `oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two`, `oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two`, `oangle_add_left_smul_rotation_pi_div_two`, `oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two`, `oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two`, `oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two`, `oangle_add_right_smul_rotation_pi_div_two`, `oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two`, `oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two`, `oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two`, `oangle_sub_left_smul_rotation_pi_div_two`, `oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two`, `oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two`, `oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two`, `oangle_sub_right_smul_rotation_pi_div_two`, `sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two`, `sin_oangle_add_left_of_oangle_eq_pi_div_two`, `sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two`, `sin_oangle_add_right_of_oangle_eq_pi_div_two`, `sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two`, `sin_oangle_sub_left_of_oangle_eq_pi_div_two`, `sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two`, `sin_oangle_sub_right_of_oangle_eq_pi_div_two`, `tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two`, `tan_oangle_add_left_of_oangle_eq_pi_div_two`, `tan_oangle_add_left_smul_rotation_pi_div_two`, `tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two`, `tan_oangle_add_right_of_oangle_eq_pi_div_two`, `tan_oangle_add_right_smul_rotation_pi_div_two`, `tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two`, `tan_oangle_sub_left_of_oangle_eq_pi_div_two`, `tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two`, `tan_oangle_sub_right_of_oangle_eq_pi_div_two`	81
Total	81

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_oangle_toReal_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` `abs` `Real.lattice` `Real.instAddGroup` `Real.Angle.toReal` `oangle`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle.congr_simp` `oangle_self_left` `Real.Angle.toReal_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsOrderedRing` `Real.instNontrivial` `oangle_self_right` `angle_eq_abs_oangle_toReal` `angle_lt_pi_div_two_of_angle_eq_pi_div_two`
`cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.cos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.cos_coe` `dist_comm` `cos_angle_mul_dist_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two`
`cos_oangle_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.cos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.cos_coe` `cos_angle_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `dist_comm`
`cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.cos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `cos_angle_mul_dist_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two`
`cos_oangle_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.cos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `cos_angle_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two`
`dist_div_cos_oangle_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.Angle.cos`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.cos_coe` `dist_comm` `dist_div_cos_angle_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`dist_div_cos_oangle_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.Angle.cos`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `dist_div_cos_angle_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `right_ne_of_oangle_eq_pi_div_two`
`dist_div_sin_oangle_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.Angle.sin`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.sin_coe` `dist_comm` `dist_div_sin_angle_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `right_ne_of_oangle_eq_pi_div_two`
`dist_div_sin_oangle_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.Angle.sin`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `dist_div_sin_angle_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`dist_div_tan_oangle_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.Angle.tan`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.tan_coe` `dist_div_tan_angle_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `right_ne_of_oangle_eq_pi_div_two`
`dist_div_tan_oangle_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.Angle.tan`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `dist_div_tan_angle_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`oangle_eq_oangle_of_two_zsmul_eq_of_angle_eq_pi_div_two` 📖	—	`Real.Angle` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instNormedAddCommGroupAngle` `oangle` `angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two` `abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two`
`oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two` 📖	—	`Real.Angle` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instNormedAddCommGroupAngle` `oangle` `angle` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two` `abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two` `oangle_rev` `Real.Angle.abs_toReal_neg`
`oangle_left_eq_arccos_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arccos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `angle_eq_arccos_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `dist_comm`
`oangle_left_eq_arcsin_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arcsin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `angle_eq_arcsin_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two` `dist_comm`
`oangle_left_eq_arctan_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arctan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `angle_eq_arctan_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`oangle_right_eq_arccos_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arccos` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_eq_arccos_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two`
`oangle_right_eq_arcsin_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arcsin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_eq_arcsin_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`oangle_right_eq_arctan_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.arctan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_eq_arctan_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `right_ne_of_oangle_eq_pi_div_two`
`sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.sin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.sin_coe` `dist_comm` `sin_angle_mul_dist_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two`
`sin_oangle_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.sin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.sin_coe` `sin_angle_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two` `dist_comm`
`sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.sin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `sin_angle_mul_dist_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two`
`sin_oangle_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.sin` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `sin_angle_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.tan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.tan_coe` `tan_angle_mul_dist_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two` `left_ne_of_oangle_eq_pi_div_two`
`tan_oangle_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.tan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `angle_comm` `Real.Angle.tan_coe` `tan_angle_of_angle_eq_pi_div_two` `angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two`
`tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.tan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `tan_angle_mul_dist_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two` `right_ne_of_oangle_eq_pi_div_two`
`tan_oangle_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.tan` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rotate_sign` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `tan_angle_of_angle_eq_pi_div_two` `angle_eq_pi_div_two_of_oangle_eq_pi_div_two`

Orientation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.cos` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two`
`cos_oangle_add_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.cos` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `cos_oangle_add_right_of_oangle_eq_pi_div_two`
`cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.cos` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two`
`cos_oangle_add_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.cos` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `InnerProductGeometry.cos_angle_add_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two`
`cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.cos` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two`
`cos_oangle_sub_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.cos` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `cos_oangle_sub_right_of_oangle_eq_pi_div_two`
`cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.cos` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two`
`cos_oangle_sub_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.cos` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `InnerProductGeometry.cos_angle_sub_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two`
`norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.cos` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two`
`norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.cos` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.cos` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two`
`norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.cos` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.cos_coe` `InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.sin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two`
`norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.sin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.sin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two`
`norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.sin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.tan` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two`
`norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.tan` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.tan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two`
`norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real.Angle.tan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arccos` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two`
`oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arcsin` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two`
`oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arctan` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two`
`oangle_add_left_smul_rotation_pi_div_two` 📖	mathematical	—	`oangle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `rotation` `Real.Angle.coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.arctan` `Real.instInv`	—	`Real.instIsStrictOrderedRing` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `oangle.congr_simp` `zero_smul` `add_zero` `oangle_zero_right` `inv_zero` `Real.arctan_zero` `oangle_rev` `oangle_neg_orientation_eq_neg` `neg_neg` `rotation_neg_orientation_eq_neg` `add_comm` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `rotation_rotation` `rotation.congr_simp` `add_neg_cancel` `rotation_zero` `inv_smul_smul₀` `oangle_add_right_smul_rotation_pi_div_two` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arccos` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two`
`oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arcsin` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.arctan` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`oangle_add_right_smul_rotation_pi_div_two` 📖	mathematical	—	`oangle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `rotation` `Real.Angle.coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.arctan`	—	`Real.instIsStrictOrderedRing` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `lt_trichotomy` `oangle_smul_right_of_neg` `oangle_neg_right` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `oangle_rotation_self_right` `sub_eq_zero` `add_comm` `sub_neg_eq_add` `Real.Angle.coe_add` `add_assoc` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `two_mul` `Real.Angle.coe_two_pi` `oangle_rev` `oangle_neg_orientation_eq_neg` `oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two` `neg_neg` `norm_smul` `NormedSpace.toNormSMulClass` `LinearIsometryEquiv.norm_map` `mul_div_assoc` `div_self` `norm_ne_zero_iff` `mul_one` `Real.norm_eq_abs` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.arctan_neg` `Real.Angle.coe_neg` `zero_smul` `add_zero` `oangle_self` `Real.arctan_zero` `Real.Angle.coe_zero` `oangle_smul_right_of_pos` `abs_of_pos`
`oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arccos` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two`
`oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arcsin` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two`
`oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arctan` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two`
`oangle_sub_left_smul_rotation_pi_div_two` 📖	mathematical	—	`oangle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `rotation` `Real.Angle.coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.arctan`	—	`Real.instIsStrictOrderedRing` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `oangle.congr_simp` `zero_smul` `sub_zero` `oangle_self` `Real.arctan_zero` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `rotation_rotation` `rotation.congr_simp` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `rotation_pi` `smul_neg` `neg_neg` `inv_smul_smul₀` `sub_eq_add_neg` `add_comm` `oangle_add_left_smul_rotation_pi_div_two` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `inv_inv`
`oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arccos` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two`
`oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arcsin` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arctan` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`oangle_sub_right_smul_rotation_pi_div_two` 📖	mathematical	—	`oangle` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `rotation` `Real.Angle.coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.arctan` `Real.instInv`	—	`Real.instIsStrictOrderedRing` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `oangle.congr_simp` `zero_smul` `zero_sub` `oangle_zero_left` `inv_zero` `Real.arctan_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `rotation_rotation` `rotation.congr_simp` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `rotation_pi` `smul_neg` `inv_smul_smul₀` `sub_eq_add_neg` `oangle_add_right_smul_rotation_pi_div_two` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.sin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two`
`sin_oangle_add_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.sin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `sin_oangle_add_right_of_oangle_eq_pi_div_two`
`sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.sin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two`
`sin_oangle_add_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.sin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `InnerProductGeometry.sin_angle_add_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.sin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two`
`sin_oangle_sub_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.sin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `sin_oangle_sub_right_of_oangle_eq_pi_div_two`
`sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.sin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two`
`sin_oangle_sub_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.sin` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.sin_coe` `InnerProductGeometry.sin_angle_sub_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.tan` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two`
`tan_oangle_add_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.tan` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `add_comm` `tan_oangle_add_right_of_oangle_eq_pi_div_two`
`tan_oangle_add_left_smul_rotation_pi_div_two` 📖	mathematical	—	`Real.Angle.tan` `oangle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `rotation` `Real.Angle.coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instInv`	—	`Real.instIsStrictOrderedRing` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `oangle_add_left_smul_rotation_pi_div_two` `Real.Angle.tan_coe` `Real.tan_arctan`
`tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.tan` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two` `left_ne_zero_of_oangle_eq_pi_div_two`
`tan_oangle_add_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.tan` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_add_right` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `InnerProductGeometry.tan_angle_add_of_inner_eq_zero` `inner_eq_zero_of_oangle_eq_pi_div_two`
`tan_oangle_add_right_smul_rotation_pi_div_two` 📖	mathematical	—	`Real.Angle.tan` `oangle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `rotation` `Real.Angle.coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Real.instIsStrictOrderedRing` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `oangle_add_right_smul_rotation_pi_div_two` `Real.Angle.tan_coe` `Real.tan_arctan`
`tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.tan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two`
`tan_oangle_sub_left_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.tan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_rev` `oangle_neg_orientation_eq_neg` `tan_oangle_sub_right_of_oangle_eq_pi_div_two`
`tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.Angle.tan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two` `right_ne_zero_of_oangle_eq_pi_div_two`
`tan_oangle_sub_right_of_oangle_eq_pi_div_two` 📖	mathematical	`oangle` `Real.Angle.coe` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.Angle.tan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `oangle_sign_sub_right_swap` `Real.Angle.sign_coe_pi_div_two` `oangle_eq_angle_of_sign_eq_one` `Real.Angle.tan_coe` `InnerProductGeometry.tan_angle_sub_of_inner_eq_zero` `inner_rev_eq_zero_of_oangle_eq_pi_div_two`

---

← Back to Index