set_smul_top_eq_span

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.set_smul_top_eq_span

English

The scalar action of a set s on the top submodule equals the span of s.

Русский

Действие множества s над верхним подмодулем равно порождающему подмодулю, порождаемому s.

LaTeX

$$$s \\cdot \\top = \\operatorname{span}(s)$$$

Lean4

@[simp]
theorem set_smul_top_eq_span (s : Set R) : s • ⊤ = Ideal.span s :=
  (span_smul_eq s ⊤).symm.trans (Ideal.span s).mul_top

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

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

Разделы

Аффилиация

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