mathlib documentation

linear_algebra.free_algebra

Linear algebra properties of free_algebra R X #

This file provides a free_monoid X basis on the free_algebra R X, and uses it to show the dimension of the algebra is the cardinality of list X

noncomputable def free_algebra.basis_free_monoid (R : Type u) (X : Type v) [comm_ring R] :

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

Equations
theorem free_algebra.dim_eq {K : Type u} {X : Type (max u v)} [field K] :