instIsPushoutFractionRingMvPolynomial

English

For any σ, the rank of FractionRing(MvPolynomial σ R) over FractionRing(MvPolynomial σ S) equals the 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}\bigl(\operatorname{Module.rank}\,R\,S\bigr)$$$

Lean4

instance {σ : Type*} : Algebra.IsPushout R (FractionRing (MvPolynomial σ R)) S (FractionRing (MvPolynomial σ S)) :=
  (Algebra.IsPushout.comp_iff _ (MvPolynomial σ R) _ (MvPolynomial σ S)).mpr inferInstance

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