nonDegenerateFlip_iff — Mathlib

English

A bilinear form B is nondegenerate if and only if its flip B.flip is nondegenerate.

Русский

Билинейная форма B невырождена тогда и только тогда, когда её перевёрнутая форма B.flip невырождена.

LaTeX

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

Lean4

theorem nonDegenerateFlip_iff {B : BilinForm K V} : B.flip.Nondegenerate ↔ B.Nondegenerate :=
  ⟨Nondegenerate.flip, Nondegenerate.flip⟩

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