# mathlibdocumentation

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
@[simp]
theorem free_algebra.basis_free_monoid_repr_symm_apply (R : Type u) (X : Type v) [comm_ring R] (ᾰ : →₀ R) :
@[simp]
theorem free_algebra.basis_free_monoid_repr_apply (R : Type u) (X : Type v) [comm_ring R] (ᾰ : X) :
theorem free_algebra.dim_eq {K : Type u} {X : Type (max u v)} [field K] :