English
For any index set σ, the rank of the MV-polynomial ring extension over R versus over S does not depend on σ: Rank_R,S equals Rank_R,S after base change.
Русский
Для множества индексов σ ранг расширения MV-полиномов над R и S не зависит от σ; ранг после базового изменения совпадает.
LaTeX
$$$\operatorname{Module.rank}\,\bigl(\operatorname{MvPolynomial}\,\sigma\,R\bigr)\bigl(\operatorname{MvPolynomial}\,\sigma\,S\bigr) = \operatorname{Module.rank}\,R\,S$$$
Lean4
theorem rank_mvPolynomial_mvPolynomial (σ : Type u) :
Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u} (Module.rank R S) :=
by
have := Algebra.isPushout_iff R (MvPolynomial σ R) S (MvPolynomial σ S) |>.mp inferInstance |>.lift_rank_eq
rwa [Cardinal.lift_id', Cardinal.lift_umax] at this
