nondegenerate_toBilin_iff — Mathlib

English

Equivalence between nondegeneracy of a BilinForm in matrix form toMatrix' and the abstract nondegeneracy.

Русский

Эквивалентность между неразложимостью билинейной формы в матричной форме toMatrix' и абстрактной неразложимостью.

LaTeX

$$$$B.Nondegenerate \iff (BilinForm.toMatrix' B).Nondegenerate.$$$$

Lean4

@[simp]
theorem _root_.Matrix.nondegenerate_toBilin_iff {M : Matrix ι ι R₂} (b : Basis ι R₂ M₂) :
    (Matrix.toBilin b M).Nondegenerate ↔ M.Nondegenerate := by
  rw [← Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, Matrix.nondegenerate_toBilin'_iff]

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