toMatrix₂' — Mathlib

English

If a bilinear form B is left-nondegenerate, then the Gram matrix of B with respect to any basis is nondegenerate.

Русский

Если билинейная форма B слева-разделяющая, то её граммова матрица по любому базису невырождена.

LaTeX

$$$ B.SeparatingLeft \Rightarrow (toMatrix_2' R_1 B).Nondegenerate $$$

Lean4

theorem toMatrix₂' {B : (ι → R₁) →ₗ[R₁] (ι → R₁) →ₗ[R₁] R₁} (h : B.SeparatingLeft) :
    (LinearMap.toMatrix₂' R₁ B).Nondegenerate :=
  nondegenerate_toMatrix₂'_iff.mpr h

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