Nondegenerate — Mathlib

English

A matrix M over a finite index set with commutative ring R is nondegenerate if for every v ≠ 0 there exists w ≠ 0 such that w^T M v ≠ 0.

Русский

Матрица M над кольцом R конечного размера не вырождается: для любого v ≠ 0 существует w ≠ 0 such that w^T M v ≠ 0.

LaTeX

$$$\text{Nondegenerate}_{m}(M) \iff \forall v\neq 0, \exists w\neq 0 : v^T M w \neq 0$$$

Lean4

/-- A matrix `M` is nondegenerate if for all `v ≠ 0`, there is a `w ≠ 0` with `w * M * v ≠ 0`. -/
def Nondegenerate [Finite m] (M : Matrix m m R) :=
  letI : Fintype m := Fintype.ofFinite m
  ∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0

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