span_span

Mathlib.LinearAlgebra.Span.Defs

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

English

Span insertion formula in duplicate form.

Русский

Формула вставки span в дубликатной форме.

LaTeX

$$$$ \\operatorname{span} R(\\operatorname{insert} x\, s) = \\operatorname{span} R s. $$$$

Lean4

theorem span_span : span R (span R s : Set M) = span R s :=
  span_eq _

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

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

Разделы

Аффилиация

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