nondegenerate_toMatrix_iff — Mathlib

English

For a bilinear form B, its Gram matrix with respect to a basis is nondegenerate if and only if B is left-nondegenerate.

Русский

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

LaTeX

$$$ (toMatrix_2 b b B).Nondegenerate \iff B.SeparatingLeft $$$

Lean4

@[simp]
theorem nondegenerate_toMatrix_iff {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :
    (toMatrix₂ b b B).Nondegenerate ↔ B.SeparatingLeft :=
  (Matrix.separatingLeft_toLinearMap₂_iff b).symm.trans <| (Matrix.toLinearMap₂_toMatrix₂ b b B).symm ▸ Iff.rfl

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