basisSingleOne — Mathlib

English

There is a canonical basis on index set ι for the finsupp R-module ι →₀ R given by the family i ↦ single i 1.

Русский

Существует каноническая база на индексовом множестве ι для модуля ι →₀ R, задаваемая семейством i ↦ single i 1.

LaTeX

$$$\\text{Finsupp.basisSingleOne}$ is a basis on $ι$ with vectors $i \\mapsto \\mathrm{single}_i(1)$$$

Lean4

/-- The basis on `ι →₀ R` with basis vectors `fun i ↦ single i 1`. -/
@[simps]
protected def basisSingleOne : Basis ι R (ι →₀ R) :=
  Basis.ofRepr (LinearEquiv.refl _ _)

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