Theorems · Definition · ring theory

FreeAlgebra.equivMonoidAlgebraFreeMonoid

{R : Type u_1} → {X : Type u_2} → [inst : CommSemiring R] → FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)

The free algebra on X is "just" the monoid algebra on the free monoid on X. This would be useful when constructing linear maps out of a free algebra, for example.

Defined in

Mathlib.Algebra.FreeAlgebra

Cited by

3 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring