nondegenerate_toMatrix₂'_iff — Mathlib

English

For a bilinear form B and a suitable finite basis, the matrix of B is nondegenerate if and only if B is SeparatingLeft (left-nondegenerate).

Русский

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

LaTeX

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

Lean4

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

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