mem_span_singleton'

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#Ideal.mem_span_singleton'

English

For any a,b in α, a ∈ span({b}) iff ∃ t, t*b = a.

Русский

Для любых a,b в α: a ∈ span({b}) эквивалентно существованию t, t*b = a.

LaTeX

$$$x \\in \\operatorname{span}(\\{y\\}) \\iff \\exists a, a \\cdot y = x$$$

Lean4

theorem mem_span_singleton' {x y : α} : x ∈ span ({ y } : Set α) ↔ ∃ a, a * y = x :=
  Submodule.mem_span_singleton

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

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

Разделы

Аффилиация

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