basisFreeMonoid — Mathlib

English

The basis on FreeMonoid X for FreeAlgebra R X is given by mapping a word [x1,...,xn] to the monomial 1 · x1 · x2 · ... · xn.

Русский

База на FreeMonoid X для FreeAlgebra R X задаётся отображением слова [x1,...,xn] в мономиал 1 · x1 · x2 · ... · xn.

LaTeX

$$$\\text{basisFreeMonoid}: \\text{Basis}(\\text{FreeMonoid}(X))\\; R\\; \\text{FreeAlgebra}(R,X)$$$

Lean4

/-- The `FreeMonoid X` basis on the `FreeAlgebra R X`,
mapping `[x₁, x₂, ..., xₙ]` to the "monomial" `1 • x₁ * x₂ * ⋯ * xₙ` -/
-- @[simps]

noncomputable def basisFreeMonoid : Basis (FreeMonoid X) R (FreeAlgebra R X) :=
  Finsupp.basisSingleOne.map (equivMonoidAlgebraFreeMonoid (R := R) (X := X)).symm.toLinearEquiv

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