Rank of multivariate rational function field

theorem MvRatFunc.rank_eq_max_lift {σ : Type u} {F : Type v} [Field F] [Nonempty σ] : Module.rank F (FractionRing (MvPolynomial σ F)) = Cardinal.lift.{u, v} (Cardinal.mk F) ⊔ Cardinal.lift.{v, u} (Cardinal.mk σ) ⊔ Cardinal.aleph0