Oriented angles in right-angled triangles.

This file proves basic geometrical results about distances and oriented angles in (possibly degenerate) right-angled triangles in real inner product spaces and Euclidean affine spaces.

theorem Orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))

An angle in a right-angled triangle expressed using arccos.

theorem Orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o (x + y) y = ↑(Real.arccos (‖y‖ / ‖x + y‖))

An angle in a right-angled triangle expressed using arccos.

theorem Orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))

An angle in a right-angled triangle expressed using arcsin.

theorem Orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))

An angle in a right-angled triangle expressed using arcsin.

theorem Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))

An angle in a right-angled triangle expressed using arctan.

theorem Orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o (x + y) y = ↑(Real.arctan (‖x‖ / ‖y‖))

An angle in a right-angled triangle expressed using arctan.

theorem Orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o x (x + y)) = ‖x‖ / ‖x + y‖

The cosine of an angle in a right-angled triangle as a ratio of sides.

theorem Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o (x + y) y) = ‖y‖ / ‖x + y‖

The cosine of an angle in a right-angled triangle as a ratio of sides.

theorem Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o x (x + y)) = ‖y‖ / ‖x + y‖

The sine of an angle in a right-angled triangle as a ratio of sides.

theorem Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o (x + y) y) = ‖x‖ / ‖x + y‖

The sine of an angle in a right-angled triangle as a ratio of sides.

theorem Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o x (x + y)) = ‖y‖ / ‖x‖

The tangent of an angle in a right-angled triangle as a ratio of sides.

theorem Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o (x + y) y) = ‖x‖ / ‖y‖

The tangent of an angle in a right-angled triangle as a ratio of sides.

theorem Orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o x (x + y)) * ‖x + y‖ = ‖x‖

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side.

theorem Orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o (x + y) y) * ‖x + y‖ = ‖y‖

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side.

theorem Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o x (x + y)) * ‖x + y‖ = ‖y‖

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side.

theorem Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o (x + y) y) * ‖x + y‖ = ‖x‖

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side.

theorem Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o x (x + y)) * ‖x‖ = ‖y‖

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side.

theorem Orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o (x + y) y) * ‖y‖ = ‖x‖

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side.

theorem Orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖x‖ / Real.Angle.cos (Orientation.oangle o x (x + y)) = ‖x + y‖

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse.

theorem Orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖y‖ / Real.Angle.cos (Orientation.oangle o (x + y) y) = ‖x + y‖

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse.

theorem Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖y‖ / Real.Angle.sin (Orientation.oangle o x (x + y)) = ‖x + y‖

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse.

theorem Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖x‖ / Real.Angle.sin (Orientation.oangle o (x + y) y) = ‖x + y‖

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse.

theorem Orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖y‖ / Real.Angle.tan (Orientation.oangle o x (x + y)) = ‖x‖

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side.

theorem Orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖x‖ / Real.Angle.tan (Orientation.oangle o (x + y) y) = ‖y‖

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side.

theorem Orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))

An angle in a right-angled triangle expressed using arccos, version subtracting vectors.

theorem Orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o (x - y) x = ↑(Real.arccos (‖x‖ / ‖x - y‖))

An angle in a right-angled triangle expressed using arccos, version subtracting vectors.

theorem Orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))

An angle in a right-angled triangle expressed using arcsin, version subtracting vectors.

theorem Orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))

An angle in a right-angled triangle expressed using arcsin, version subtracting vectors.

theorem Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))

An angle in a right-angled triangle expressed using arctan, version subtracting vectors.

theorem Orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Orientation.oangle o (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))

An angle in a right-angled triangle expressed using arctan, version subtracting vectors.

theorem Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o y (y - x)) = ‖y‖ / ‖y - x‖

The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem Orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o (x - y) x) = ‖x‖ / ‖x - y‖

The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o y (y - x)) = ‖x‖ / ‖y - x‖

The sine of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o (x - y) x) = ‖y‖ / ‖x - y‖

The sine of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o y (y - x)) = ‖x‖ / ‖y‖

The tangent of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem Orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o (x - y) x) = ‖y‖ / ‖x‖

The tangent of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o y (y - x)) * ‖y - x‖ = ‖y‖

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side, version subtracting vectors.

theorem Orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.cos (Orientation.oangle o (x - y) x) * ‖x - y‖ = ‖x‖

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side, version subtracting vectors.

theorem Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o y (y - x)) * ‖y - x‖ = ‖x‖

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side, version subtracting vectors.

theorem Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.sin (Orientation.oangle o (x - y) x) * ‖x - y‖ = ‖y‖

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side, version subtracting vectors.

theorem Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o y (y - x)) * ‖y‖ = ‖x‖

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side, version subtracting vectors.

theorem Orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : Real.Angle.tan (Orientation.oangle o (x - y) x) * ‖x‖ = ‖y‖

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side, version subtracting vectors.

theorem Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖y‖ / Real.Angle.cos (Orientation.oangle o y (y - x)) = ‖y - x‖

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse, version subtracting vectors.

theorem Orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖x‖ / Real.Angle.cos (Orientation.oangle o (x - y) x) = ‖x - y‖

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse, version subtracting vectors.

theorem Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖x‖ / Real.Angle.sin (Orientation.oangle o y (y - x)) = ‖y - x‖

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse, version subtracting vectors.

theorem Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖y‖ / Real.Angle.sin (Orientation.oangle o (x - y) x) = ‖x - y‖

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse, version subtracting vectors.

theorem Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖x‖ / Real.Angle.tan (Orientation.oangle o y (y - x)) = ‖y‖

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side, version subtracting vectors.

theorem Orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (h : Orientation.oangle o x y = ↑(Real.pi / 2)) : ‖y‖ / Real.Angle.tan (Orientation.oangle o (x - y) x) = ‖x‖

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side, version subtracting vectors.

theorem Orientation.oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (h : x ≠ 0) (r : ℝ) : Orientation.oangle o x (x + r • (Orientation.rotation o ↑(Real.pi / 2)) x) = ↑(Real.arctan r)

An angle in a right-angled triangle expressed using arctan, where one side is a multiple of a rotation of another by π / 2.

theorem Orientation.oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (h : x ≠ 0) (r : ℝ) : Orientation.oangle o (x + r • (Orientation.rotation o ↑(Real.pi / 2)) x) (r • (Orientation.rotation o ↑(Real.pi / 2)) x) = ↑(Real.arctan r⁻¹)

An angle in a right-angled triangle expressed using arctan, where one side is a multiple of a rotation of another by π / 2.

theorem Orientation.tan_oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (h : x ≠ 0) (r : ℝ) : Real.Angle.tan (Orientation.oangle o x (x + r • (Orientation.rotation o ↑(Real.pi / 2)) x)) = r

The tangent of an angle in a right-angled triangle, where one side is a multiple of a rotation of another by π / 2.

theorem Orientation.tan_oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (h : x ≠ 0) (r : ℝ) : Real.Angle.tan (Orientation.oangle o (x + r • (Orientation.rotation o ↑(Real.pi / 2)) x) (r • (Orientation.rotation o ↑(Real.pi / 2)) x)) = r⁻¹

The tangent of an angle in a right-angled triangle, where one side is a multiple of a rotation of another by π / 2.

theorem Orientation.oangle_sub_right_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (h : x ≠ 0) (r : ℝ) : Orientation.oangle o (r • (Orientation.rotation o ↑(Real.pi / 2)) x) (r • (Orientation.rotation o ↑(Real.pi / 2)) x - x) = ↑(Real.arctan r⁻¹)

An angle in a right-angled triangle expressed using arctan, where one side is a multiple of a rotation of another by π / 2, version subtracting vectors.

theorem Orientation.oangle_sub_left_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (h : x ≠ 0) (r : ℝ) : Orientation.oangle o (x - r • (Orientation.rotation o ↑(Real.pi / 2)) x) x = ↑(Real.arctan r)

An angle in a right-angled triangle expressed using arctan, where one side is a multiple of a rotation of another by π / 2, version subtracting vectors.

theorem EuclideanGeometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))

An angle in a right-angled triangle expressed using arccos.

theorem EuclideanGeometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))

An angle in a right-angled triangle expressed using arccos.

theorem EuclideanGeometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))

An angle in a right-angled triangle expressed using arcsin.

theorem EuclideanGeometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))

An angle in a right-angled triangle expressed using arcsin.

theorem EuclideanGeometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))

An angle in a right-angled triangle expressed using arctan.

theorem EuclideanGeometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))

An angle in a right-angled triangle expressed using arctan.

theorem EuclideanGeometry.cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.cos (EuclideanGeometry.oangle p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

The cosine of an angle in a right-angled triangle as a ratio of sides.

theorem EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.cos (EuclideanGeometry.oangle p₃ p₁ p₂) = dist p₁ p₂ / dist p₁ p₃

The cosine of an angle in a right-angled triangle as a ratio of sides.

theorem EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.sin (EuclideanGeometry.oangle p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

The sine of an angle in a right-angled triangle as a ratio of sides.

theorem EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.sin (EuclideanGeometry.oangle p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₃

The sine of an angle in a right-angled triangle as a ratio of sides.

theorem EuclideanGeometry.tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.tan (EuclideanGeometry.oangle p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂

The tangent of an angle in a right-angled triangle as a ratio of sides.

theorem EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.tan (EuclideanGeometry.oangle p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₂

The tangent of an angle in a right-angled triangle as a ratio of sides.

theorem EuclideanGeometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.cos (EuclideanGeometry.oangle p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side.

theorem EuclideanGeometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.cos (EuclideanGeometry.oangle p₃ p₁ p₂) * dist p₁ p₃ = dist p₁ p₂

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side.

theorem EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.sin (EuclideanGeometry.oangle p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side.

theorem EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.sin (EuclideanGeometry.oangle p₃ p₁ p₂) * dist p₁ p₃ = dist p₃ p₂

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side.

theorem EuclideanGeometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.tan (EuclideanGeometry.oangle p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side.

theorem EuclideanGeometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : Real.Angle.tan (EuclideanGeometry.oangle p₃ p₁ p₂) * dist p₁ p₂ = dist p₃ p₂

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side.

theorem EuclideanGeometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₃ p₂ / Real.Angle.cos (EuclideanGeometry.oangle p₂ p₃ p₁) = dist p₁ p₃

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse.

theorem EuclideanGeometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₁ p₂ / Real.Angle.cos (EuclideanGeometry.oangle p₃ p₁ p₂) = dist p₁ p₃

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse.

theorem EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₁ p₂ / Real.Angle.sin (EuclideanGeometry.oangle p₂ p₃ p₁) = dist p₁ p₃

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse.

theorem EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₃ p₂ / Real.Angle.sin (EuclideanGeometry.oangle p₃ p₁ p₂) = dist p₁ p₃

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse.

theorem EuclideanGeometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₁ p₂ / Real.Angle.tan (EuclideanGeometry.oangle p₂ p₃ p₁) = dist p₃ p₂

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side.

theorem EuclideanGeometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : dist p₃ p₂ / Real.Angle.tan (EuclideanGeometry.oangle p₃ p₁ p₂) = dist p₁ p₂

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side.