instIsPrincipalSpanSingletonSet

Mathlib.LinearAlgebra.Span.Defs

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

English

If S is a principal submodule, there exists an element generator(S) ∈ M such that span{ generator(S) } = S.

Русский

Если S — главный (principal) подпредмодуль, то существует элемент generator(S) ∈ M такой, что span{generator(S)} = S.

LaTeX

$$$ generator(S) \in M \quad \text{and} \quad \operatorname{span} R\{ generator(S) \} = S. $$$

Lean4

instance (x : R) : (span R { x }).IsPrincipal :=
  ⟨x, rfl⟩

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

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

Разделы

Аффилиация

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