ofList

Mathlib.RingTheory.Regular.RegularSequence

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

English

The ideal generated by a list rs is the span of the set { r | r ∈ rs }.

Русский

Идеал, порожденный списком rs, равен области порожденной множеством { r | r ∈ rs }.

LaTeX

$$$\\text{Ideal.ofList}(rs) = \\operatorname{span} \\{ r \\mid r \\in rs \\}$$$

Lean4

/-- The ideal generated by a list of elements. -/
abbrev ofList (rs : List R) :=
  span {r | r ∈ rs}

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

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

Разделы

Аффилиация

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