span_empty

Mathlib.LinearAlgebra.Span.Defs

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

English

Spanning the empty set gives the bottom submodule.

Русский

Порождающее пустое множество дает нулевой подмодуль.

LaTeX

$$$$\operatorname{span} R (\varnothing) = \bot$$$$

Lean4

@[simp]
theorem span_empty : span R (∅ : Set M) = ⊥ :=
  (Submodule.gi R M).gc.l_bot

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

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

Разделы

Аффилиация

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