ofList_singleton

Mathlib.RingTheory.Regular.RegularSequence

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

English

The ideal generated by a singleton [r] equals the span of { r }.

Русский

Идеал, порожденный единичным списком [r], равен области порождающей { r }.

LaTeX

$$$\\text{Ideal.ofList}([r]) = \\operatorname{span}\\{ r \\}$$$

Lean4

theorem ofList_singleton (r : R) : ofList [r] = span { r } :=
  congrArg span (Set.ext fun _ => List.mem_singleton)

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

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

Разделы

Аффилиация

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