toMatrix₂ — Mathlib

English

If a bilinear form B is left-nondegenerate, then its associated matrix with respect to a chosen basis is nondegenerate.

Русский

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

LaTeX

$$(h : B.SeparatingLeft) (b) → (toMatrix₂' R_1 B).Nondegenerate$$

Lean4

theorem toMatrix₂ {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (h : B.SeparatingLeft) (b : Basis ι R₁ M₁) :
    (toMatrix₂ b b B).Nondegenerate :=
  (nondegenerate_toMatrix_iff b).mpr h

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