finrank_eq

Mathlib.LinearAlgebra.Dimension.Localization

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

English

For a base change bc, the lifted ranks of P and M coincide: lift(rank_T P) = lift(rank_R M).

Русский

При базовом изменении bc ранги поднимаются и равны: lift(rank_T P) = lift(rank_R M).

LaTeX

$$$\operatorname{lift}\big(\operatorname{Module.rank} T P\big) = \operatorname{lift}\big(\operatorname{Module.rank} R M\big)$$$

Lean4

theorem finrank_eq : finrank T P = finrank R M := by simpa using congr_arg toNat bc.lift_rank_eq

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

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

Разделы

Аффилиация

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