linearIndependent — Mathlib

English

A basis yields a linearly independent family of vectors: the basis vectors are linearly independent.

Русский

Базис образует линейно независимый набор векторов: векторы базиса линейно независимы.

LaTeX

$$$\text{LinearIndependent}(R, b)$.$$

Lean4

protected theorem linearIndependent : LinearIndependent R b := fun x y hxy => by
  rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]

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