span_singleton_one

Mathlib.RingTheory.Ideal.Span

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

English

The span of {1} is the top ideal.

Русский

Покрытие {1} равно верхнему идеалу.

LaTeX

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

Lean4

@[simp]
theorem span_singleton_one : span ({ 1 } : Set α) = ⊤ :=
  (eq_top_iff_one _).2 <| subset_span <| mem_singleton _

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

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

Разделы

Аффилиация

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