rank_fractionRing_polynomial — Mathlib

English

If R → S is an algebraic domain setup with faithful scalar action, then the rank of FractionRing(Polynomial R) over FractionRing(Polynomial S) equals the rank of R over S.

Русский

При алгебраическом отношении R к S и верном действии скаляра ранг дробной кольцевой оболочки Polynomial определяется как ранг исходного расширения R→S.

LaTeX

$$$\\operatorname{Module.rank}(\\FractionRing(\\operatorname{Polynomial} R))(\\FractionRing(\\operatorname{Polynomial} S)) = \\operatorname{Module.rank} R S.$$$

Lean4

@[stacks 0G1M]
theorem rank_fractionRing_polynomial : Module.rank (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S :=
  by
  have := (FaithfulSMul.algebraMap_injective R S).isDomain
  rw [rank_fractionRing, rank_polynomial_polynomial]

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