rank_fractionRing — Mathlib

English

If R,S are rings with a fraction ring relation and S′ is the corresponding extension, then the rank over the fraction rings matches the base rank, i.e., Module.rank (FractionRing R) (FractionRing S) = Module.rank R S.

Русский

Если S и R связаны дробными кольцами, то ранг над дробными кольцами совпадает с базовым рангом: Module.rank (FractionRing R) (FractionRing S) = Module.rank R S.

LaTeX

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

Lean4

theorem rank_fractionRing [IsDomain S] : Module.rank (FractionRing R) (FractionRing S) = Module.rank R S :=
  rank_of_isFractionRing ..

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