English
Let R be a commutative ring and X a set. The rank of FreeAlgebra_R(X) as an R-module equals lift(|List(X)|), i.e., the number of finite words over X.
Русский
Пусть R — коммутативное кольцо, X — множество. Ранг свободной алгебры над R на X как R-модуля равен lift(|List(X)|), т.е. количеству конечных слов над X.
LaTeX
$$$$ \operatorname{rank}_R\big( \mathrm{FreeAlgebra}_R(X) \big) = \operatorname{lift}\big( |\mathrm{List}(X)| \big) $$$$
Lean4
theorem rank_eq [CommRing R] [Nontrivial R] :
Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u} (Cardinal.mk (List X)) := by
rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _), Cardinal.lift_umax.{v, u},
FreeMonoid]
