spanRank_bot

Mathlib.Algebra.Module.SpanRank

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

English

As a simp lemma, spanRank zero is equivalent to equality with the bottom submodule.

Русский

Как упрощение, spanRank = 0 эквивалентно равенству нижнему подпространению.

LaTeX

$$@[simp] theorem spanRank_eq_zero_iff_eq_bot {I : Submodule R M} : I.spanRank = 0 ↔ I = ⊥$$

Lean4

@[simp]
theorem spanRank_bot : (⊥ : Ideal R).spanRank = 0 :=
  Submodule.spanRank_eq_zero_iff_eq_bot.mpr rfl

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

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

Разделы

Аффилиация

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