length_bot

Mathlib.RingTheory.Length

URI: https://scilib.ai/kg/mathlib#Module.length_bot

English

The length of the bottom submodule is zero: length(R, ⊥) = 0.

Русский

Длина нижнего подмодуля равна нулю: length(R, ⊥) = 0.

LaTeX

$$$\operatorname{length}(R, \bot) = 0.$$$

Lean4

theorem length_bot : Module.length R (⊥ : Submodule R M) = 0 :=
  Module.length_eq_zero

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

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

Разделы

Аффилиация

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