English
Let R be a commutative semiring and X a type. The free algebra on X over R has a free structure as an R-module; equivalently, it is canonically isomorphic (as an R-module) to the monoid algebra of the free monoid on X.
Русский
Пусть R — коммутативное полукольцо и X — множество. Свободная алгебра над R на X имеет структуру свободного R-модуля; эквивалентно она канонически изоморфна как R-модуль моноидной алгебре на свободном моноиде над X.
LaTeX
$$$$ \mathrm{FreeAlgebra}_R(X) \cong_R \mathrm{MonoidAlgebra}_R(\mathrm{FreeMonoid}(X)) $$$$
Lean4
instance : Module.Free R (FreeAlgebra R X) :=
have : Module.Free R (MonoidAlgebra R (FreeMonoid X)) := Module.Free.finsupp _ _ _
Module.Free.of_equiv (equivMonoidAlgebraFreeMonoid (R := R) (X := X)).symm.toLinearEquiv
