inner_eq_zero_symm — Mathlib

English

There is an IsSymm instance for all index sets in terms of inner products of a family of vectors; i.e., symmetry holds pointwise.

Русский

Существует инстанс IsSymm для всей совокупности индексов в терминах скалярного произведения семейства векторов; симметрия выполняется по точкам.

LaTeX

$$IsSymm ι fun i j => ⟪v_i, v_j⟫ = 0$$

Lean4

theorem inner_eq_zero_symm {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0 :=
  by
  rw [← inner_conj_symm]
  exact star_eq_zero

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