rank_le

Mathlib.LinearAlgebra.Dimension.Basic

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

English

For any submodule s, rank(s) ≤ rank(M).

Русский

Для любого подмодуля s выполняется неравенство ранга: ранг(s) ≤ ранг(M).

LaTeX

$$$\operatorname{Module.rank} R s \le \operatorname{Module.rank} R M$$$

Lean4

theorem rank_le (s : Submodule R M) : Module.rank R s ≤ Module.rank R M :=
  by
  rw [← rank_top R M]
  exact rank_mono le_top

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

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

Разделы

Аффилиация

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