norm_div_tan_angle_add_of_inner_eq_zero

English

For ⟪x, y⟫ = 0 and x ≠ 0 ∨ y ≠ 0, then ||y|| / tan(angle(x, x + y)) = ||x||.

Русский

Для ⟪x, y⟫ = 0 и x ≠ 0 или y ≠ 0: ||y|| / tan(angle(x, x + y)) = ||x||.

LaTeX

$$$$ \frac{\|y\|}{\tan\big( \angle x (x+y) \big)} = \|x\| $$$$

Lean4

/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side. -/
theorem norm_div_tan_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖ :=
  by
  rw [tan_angle_add_of_inner_eq_zero h]
  rcases h0 with (h0 | h0)
  · simp [h0]
  · rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Похожие утверждения