inner_conj_symm

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#inner_conj_symm

English

There is an IsSymm instance on inner products: for any v, the bilinear form (i,j) ↦ ⟪v_i, v_j⟫ is symmetric.

Русский

Существует инстанс симметричности для скалярного произведения: ⟪v_i, v_j⟫ = ⟪v_j, v_i⟫.

LaTeX

$$IsSymm ι (i,j) ↦ ⟪v_i, v_j⟫ = 0$$

Lean4

@[simp]
theorem inner_conj_symm (x y : E) : ⟪y, x⟫† = ⟪x, y⟫ :=
  InnerProductSpace.conj_inner_symm _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru