span_singleton_generator

Mathlib.LinearAlgebra.Span.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.IsPrincipal.span_singleton_generator

English

For a principal submodule S, the span of its generator equals S.

Русский

Для principal-подмодуля S промежуточное объединение порождающего равняется S.

LaTeX

$$$ \operatorname{span} R\{ generator(S) \} = S. $$$

Lean4

theorem span_singleton_generator (S : Submodule R M) [S.IsPrincipal] : span R {generator S} = S :=
  (Classical.choose_spec (principal S)).symm

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

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

Разделы

Аффилиация

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