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

def free_algebra.basis_free_monoid (R : Type u_1) (X : Type u_2) [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_1} {X : Type (max u_1 u_2)} [field K] :