rank_eq

Mathlib.LinearAlgebra.Dimension.Localization

URI: https://scilib.ai/kg/mathlib#IsBaseChange.rank_eq

← MathLib Explorer

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 {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 bc.lift_rank_eq

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru