fg_span_singleton

Mathlib.RingTheory.Finiteness.Basic

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

English

The submodule generated by a single element x is finitely generated.

Русский

Подмодуль, порожденный одним элементом x, конечно порожден.

LaTeX

$$$\mathrm{FG}(R \cdot x)$$$

Lean4

theorem fg_span_singleton (x : M) : FG (R ∙ x) :=
  fg_span (finite_singleton x)

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

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

Разделы

Аффилиация

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