linearIndependent_single_one — Mathlib

English

For any index type ι and a ring R, the family i ↦ single i (1: R) is linearly independent.

Русский

Для любого индексового типа ι и кольца R семейство i ↦ single i (1) линейно независимо.

LaTeX

$$$\\text{LinearIndependent } R\\; \\lambda i. \\mathrm{single}_i(1)$$$

Lean4

theorem linearIndependent_single_one : LinearIndependent R fun i : ι ↦ single i (1 : R) :=
  Finsupp.basisSingleOne.linearIndependent

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