rank_eq — Mathlib

English

Let p and f and the IsLocalizedModule hypothesis hold as above; then for any N with R-module structure, Module.rank R N = Module.rank R M.

Русский

Пусть дано p, f и условие IsLocalizedModule; тогда для любого N с модулем над R выполняется равенство рангов: Module.rank_R(N) = Module.rank_R(M).

LaTeX

$$$\operatorname{Module.rank} R N = \operatorname{Module.rank} R M$$$

Lean4

theorem rank_eq {N : Type uM} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) [IsLocalizedModule p f] :
    Module.rank R N = Module.rank R M := by simpa using lift_rank_eq p f hp

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