English
Let η be a finite index set and M an R-vector space. Then the dimension (rank) of the space of all functions η → M over R equals the cardinality of η times the dimension of M, i.e., dim_R(η → M) = |η| · dim_R M (with the standard universe lift on the right-hand side).
Русский
Пусть η — конечный индексный множество, M — R-векторное пространство. Тогда размерность пространства функций η → M равна произведению модуляции η на размерность M: dim_R(η → M) = |η| · dim_R M (с учётом соответствующего переноса кардиналов).
LaTeX
$$$ \\operatorname{Module.rank} R (\\eta \\to M) = (\\lvert \\eta \\rvert : \\operatorname{Cardinal}) \\cdot \\operatorname{Cardinal.lift} (\\operatorname{Module.rank} R M). $$$
Lean4
theorem rank_fun_eq_lift_mul :
Module.rank R (η → M) = (Fintype.card η : Cardinal.{max u₁' v}) * Cardinal.lift.{u₁'} (Module.rank R M) := by
rw [rank_pi, Cardinal.sum_const, Cardinal.mk_fintype, Cardinal.lift_natCast]
