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
theorem
free_algebra.is_basis_free_monoid
(R : Type u_1)
(X : Type u_2)
[comm_ring R] :
is_basis R (λ (x : free_monoid X), ⇑(⇑free_monoid.lift (free_algebra.ι R)) x)
theorem
free_algebra.dim_eq
{K : Type u_1}
{X : Type (max u_1 u_2)}
[field K] :
vector_space.dim K (free_algebra K X) = # (list X)