norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two

English

The squared norm of the sum equals the sum of squared norms when angle is π/2: ‖x+y‖^2 = ‖x‖^2 + ‖y‖^2.

Русский

...

LaTeX

$$‖x + y‖^2 = ‖x‖^2 + ‖y‖^2 ↔ angle x y = π/2$$

Lean4

/-- Pythagorean theorem, if-and-only-if vector angle form. -/
theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two (x y : V) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2 :=
  by
  rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
  exact inner_eq_zero_iff_angle_eq_pi_div_two x y

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