span_one

Mathlib.RingTheory.Ideal.Span

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

English

The submodule generated by the singleton {1} is the top submodule.

Русский

Порождение единицы образует верхний подмодуль.

LaTeX

$$$$ \operatorname{span}(\{1\}) = \top $$$$

Lean4

@[simp]
theorem span_one : span (1 : Set α) = ⊤ := by rw [← Set.singleton_one, span_singleton_one]

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

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

Разделы

Аффилиация

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