nondegenerate_def — Mathlib

English

M.Nondegenerate holds exactly when for every v, if v^T M w = 0 for all w, then v = 0.

Русский

M.Nondegenerate эквивалентно условию: для каждого v, если v^T M w = 0 для всех w, то v = 0.

LaTeX

$$$M.Nondegenerate \iff \forall v, (\forall w, v \cdot M w = 0) \rightarrow v = 0$$$

Lean4

theorem nondegenerate_def {M : Matrix m m R} : M.Nondegenerate ↔ ∀ v, (∀ w, v ⬝ᵥ M *ᵥ w = 0) → v = 0 := by
  refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩ <;> convert hv

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