mem_span_singleton_self

Mathlib.RingTheory.Ideal.Span

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

English

For any x in α, x lies in span of {x}.

Русский

Для любого x в α верно, что x ∈ span( {x} ).

LaTeX

$$$x \\in \\operatorname{span}(\\{x\\})$$$

Lean4

theorem mem_span_singleton_self (x : α) : x ∈ span ({ x } : Set α) :=
  Submodule.mem_span_singleton_self x

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

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

Разделы

Аффилиация

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