corootSpan_map_flip_toPerfPair — Mathlib

English

The scalar action of the coroot on x interacts with B to give twice the bilinear form on x and y.

Русский

Действие скаляра на корoot по отношению к x даёт двойную величину двойной формы на x и y.

LaTeX

$$B x x \cdot coroot B hx y = 2 \cdot B x y$$

Lean4

@[simp]
theorem corootSpan_map_flip_toPerfPair :
    (P.corootSpan R).map P.toLinearMap.flip.toPerfPair = span R (range P.coroot') :=
  P.flip.rootSpan_map_toPerfPair

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