basisSingleOne — Mathlib

English

The natural basis of SkewMonoidAlgebra k G is given by the basis vectors δ_g corresponding to a single g ∈ G with coefficient 1, i.e., delta-basis.

Русский

Естественная база SkewMonoidAlgebra k G задаётся базисными векторами δ_g, соответствующими одиничному элементу g ∈ G с коэффициентом 1 (дельта-база).

LaTeX

$$$ \text{basisSingleOne } : \text{Module.Basis } G k (SkewMonoidAlgebra k G) $ with repr = toFinsuppLinearEquiv$$

Lean4

/-- The basis on `SkewMonoidAlgebra k G` with basis vectors `fun i ↦ single i 1` -/
def basisSingleOne [Semiring k] : Module.Basis G k (SkewMonoidAlgebra k G) where repr := toFinsuppLinearEquiv

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