span_univ

Mathlib.RingTheory.Ideal.Span

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

English

The span of the universal set is the top element of the lattice of submodules/ideals.

Русский

Покрытие множества единицы совпадает с верхним элементом решетки подмодулей/идеалов.

LaTeX

$$$\\operatorname{span}(\\operatorname{Set.univ}) = \\top$$$

Lean4

@[simp]
theorem span_univ : span (Set.univ : Set α) = ⊤ :=
  Submodule.span_univ

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

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

Разделы

Аффилиация

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