span_zero

Mathlib.RingTheory.Ideal.Span

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

English

Let α be a semiring. The submodule of α generated by {0} is the zero submodule.

Русский

Пусть α — полугруппа с умножением и сложением. Подмодуль, порожденный множеством {0}, является нулевым подмодулем.

LaTeX

$$$$ \operatorname{span} \{0\} = \bot $$$$

Lean4

@[simp]
theorem span_zero : span (0 : Set α) = ⊥ := by rw [← Set.singleton_zero, span_singleton_eq_bot]

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

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

Разделы

Аффилиация

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