associated_isOrtho — Mathlib

English

Orthogonality is symmetric: IsOrtho Q x y iff IsOrtho Q y x.

Русский

Ортогональность симметрична: IsOrtho Q x y ⇔ IsOrtho Q y x.

LaTeX

$$$\\mathrm{IsOrtho}(Q,x,y) \\iff \\mathrm{IsOrtho}(Q,y,x).$$$

Lean4

@[simp]
theorem associated_isOrtho [Invertible (2 : R)] {x y : M} : Q.associated.IsOrtho x y ↔ Q.IsOrtho x y := by
  simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff, smul_zero, sub_sub, sub_eq_zero]

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