innerSL_real_flip — Mathlib

English

In the real case, the flip of inner product is the same as inner product with arguments swapped: innerₗ.flip = innerₗ.

Русский

В вещественном случае разворот скалярного произведения совпадает с самим скалярным произведением: innerₗ.flip = innerₗ.

LaTeX

$$$ (inner_\\ell F).flip = inner_\\ell F $$$

Lean4

@[simp]
theorem innerSL_real_flip : (innerSL ℝ (E := F)).flip = innerSL ℝ (E := F) :=
  by
  ext v w
  exact real_inner_comm _ _

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