Documentation

Mathlib.LinearAlgebra.FreeAlgebra

Linear algebra properties of FreeAlgebra R X #

This file provides a FreeMonoid X basis on the FreeAlgebra R X, and uses it to show the dimension of the algebra is the cardinality of List X

noncomputable def FreeAlgebra.basisFreeMonoid (R : Type u) (X : Type v) [CommSemiring R] :

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

Equations
Instances For
    instance FreeAlgebra.instFree (R : Type u) (X : Type v) [CommSemiring R] :
    Equations
    • =