nondegenerate_toMatrix_iff — Mathlib

English

The nondegeneracy of a bilinear form equals the nondegeneracy of its matrix form under a basis.

Русский

Неразложимость билинейной формы равна неразложимости её матричной формы в данной базе.

LaTeX

$$$$\text{(BilinForm.toMatrix' B)}\text{ Nondegenerate} \iff B.Nondegenerate.$$$$

Lean4

@[simp]
theorem nondegenerate_toMatrix_iff {B : BilinForm R₂ M₂} (b : Basis ι R₂ M₂) :
    (BilinForm.toMatrix b B).Nondegenerate ↔ B.Nondegenerate :=
  (Matrix.nondegenerate_toBilin_iff b).symm.trans <| (Matrix.toBilin_toMatrix b B).symm ▸ Iff.rfl

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