rank_fractionRing_mvPolynomial — Mathlib

English

For any σ, the rank of FractionRing(MvPolynomial σ R) over FractionRing(MvPolynomial σ S) equals lift of rank(R,S).

Русский

Для любого σ ранг FractionRing(MvPolynomial σ R) над FractionRing(MvPolynomial σ S) равен lift рангу(R,S).

LaTeX

$$$\operatorname{Module.rank}\,(\operatorname{FractionRing}(\operatorname{MvPolynomial}\;σ\;R))\, (\operatorname{FractionRing}(\operatorname{MvPolynomial}\;σ\;S)) = \operatorname{lift}(\operatorname{Module.rank}\;R\;S)$$$

Lean4

@[stacks 0G1M]
theorem rank_fractionRing_mvPolynomial (σ : Type u) :
    Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u} (Module.rank R S) :=
  by
  have := (FaithfulSMul.algebraMap_injective R S).isDomain
  rw [rank_fractionRing, rank_mvPolynomial_mvPolynomial]

Похожие утверждения