Linear algebra properties of free_algebra R X #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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] :
basis (free_monoid X) R (free_algebra R X)
The free_monoid X basis on the free_algebra R X,
mapping [x₁, x₂, ..., xₙ] to the "monomial" 1 • x₁ * x₂ * ⋯ * xₙ
@[simp]
theorem
free_algebra.basis_free_monoid_repr_symm_apply
(R : Type u)
(X : Type v)
[comm_ring R]
(ᾰ : free_monoid X →₀ R) :
@[simp]
theorem
free_algebra.basis_free_monoid_repr_apply
(R : Type u)
(X : Type v)
[comm_ring R]
(ᾰ : free_algebra R X) :
theorem
free_algebra.rank_eq
{K : Type u}
{X : Type (max u v)}
[field K] :
module.rank K (free_algebra K X) = cardinal.mk (list X)