span_empty

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#Ideal.span_empty

English

The span of the empty set is the bottom element (zero) of the lattice of submodules/ideals.

Русский

Покрытие пустого множества является наименьшим элементом (нулем) в решётке подмодулей/идеалов.

LaTeX

$$$\\operatorname{span}(\\emptyset) = \\bot$$$

Lean4

@[simp]
theorem span_empty : span (∅ : Set α) = ⊥ :=
  Submodule.span_empty

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

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

Разделы

Аффилиация

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