rank_quotient_add_rank

Mathlib.LinearAlgebra.Dimension.RankNullity

URI: https://scilib.ai/kg/mathlib#Submodule.rank_quotient_add_rank

← MathLib Explorer

English

For any submodule N ≤ M, rank_R(M/N) + rank_R(N) = rank_R(M).

Русский

Для любого подмодуля N ⊆ M выполняется rank_R(M/N) + rank_R(N) = rank_R(M).

LaTeX

$$$\operatorname{Module.rank} R (M / N) + \operatorname{Module.rank} R N = \operatorname{Module.rank} R M$$$

Lean4

theorem rank_quotient_add_rank (N : Submodule R M) : Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M :=
  HasRankNullity.rank_quotient_add_rank N

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

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

Разделы

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

Аффилиация

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