finrank — Mathlib

English

If a family b is linearly independent, the finrank of span of its range equals the size of the index set (cardinality of the index type).

Русский

Если семейство векторов линейно независимо, размерность пространства span набора их диапазона равна размерности множества индексов.

LaTeX

$$$ [\\text{Nontrivial } R] \\; \\{\\iota : Type^* \\} \\; [Fintype \\iota] \\; \\{b : \\iota \\to M\\} (hb : LinearIndependent R b) : \\; \\operatorname{finrank} R (\\operatorname{span}_R (\\operatorname{Set.range} b)) = Fintype.card \\iota. $$$

Lean4

/-- The rank of a set of vectors as a natural number. -/
protected noncomputable def finrank (s : Set M) : ℕ :=
  finrank R (span R s)

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