finrank_top

Mathlib.LinearAlgebra.Dimension.Finrank

URI: https://scilib.ai/kg/mathlib#finrank_top

English

The finrank of the top submodule equals the finrank of M.

Русский

Финранк верхнего подмодуля равен финранку M.

LaTeX

$$$\\operatorname{finrank}_R (\\top : \\text{Submodule } R M) = \\operatorname{finrank}_R M$$$

Lean4

@[simp]
theorem finrank_top : finrank R (⊤ : Submodule R M) = finrank R M :=
  by
  unfold finrank
  simp

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

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

Разделы

Аффилиация

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