rank_of_isFractionRing — Mathlib

English

If R′ is a fraction ring of R and S′ is the corresponding extension of S, then the rank of S′ over R′ equals the rank of S over R.

Русский

Если R′ — дробное кольцо от R, а S′ — соответствующее расширение S, то размерность (rank) S′ как модуль над R′ равна rank(S) над R.

LaTeX

$$$\operatorname{Module.rank}\,R',S' = \operatorname{Module.rank}\,R,S$$$

Lean4

theorem rank_of_isFractionRing (S' : Type u) [CommRing S'] [Algebra R S'] [Algebra S S'] [Module R' S']
    [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'] : Module.rank R' S' = Module.rank R S := by
  simpa using lift_rank_of_isFractionRing R R' S S'

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