# 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

theorem free_algebra.is_basis_free_monoid (R : Type u_1) (X : Type u_2) [comm_ring R] :
(λ (x : , x)
theorem free_algebra.dim_eq {K : Type u_1} {X : Type (max u_1 u_2)} [field K] :
X) = # (list X)