flip — Mathlib

English

If B is a nondegenerate bilinear form on V, then the flipped bilinear form B.flip, defined by B.flip(x,y)=B(y,x), is also nondegenerate.

Русский

Если B — невырожденная билинейная форма на V, то перевёрнутая форма B.flip, определяемая как B.flip(x,y)=B(y,x), также невырожденна.

LaTeX

$$$\\operatorname{Nondegenerate}(B) \\implies \\operatorname{Nondegenerate}(B^{\\mathrm{flip}}).$$$

Lean4

theorem flip {B : BilinForm K V} (hB : B.Nondegenerate) : B.flip.Nondegenerate :=
  by
  intro x hx
  apply (Module.evalEquiv K V).injective
  ext f
  obtain ⟨y, rfl⟩ := (B.toDual hB).surjective f
  simpa using hx y

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