rank_eq_of_le_nonZeroDivisors — Mathlib

English

Under IsBaseChange with localization, finrank_T P = finrank_R M.

Русский

При базовом изменении с локализацией finrank_T P = finrank_R M.

LaTeX

$$$\operatorname{finrank} T P = \operatorname{finrank} R M$$$

Lean4

theorem rank_eq_of_le_nonZeroDivisors {P : Type uM} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P]
    {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Module.rank T P = Module.rank R M := by
  simpa using lift_rank_eq_of_le_nonZeroDivisors S f hp hpT bc

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