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

theorem free_algebra.is_basis_free_monoid (R : Type u_1) (X : Type u_2) [comm_ring R] :
theorem free_algebra.dim_eq {K : Type u_1} {X : Type (max u_1 u_2)} [field K] :