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)) = max (max (Cardinal.lift.{u, v} (Cardinal.mk F)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0