span_singleton_smul_eq

Mathlib.LinearAlgebra.Span.Defs

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

← MathLib Explorer

English

span R (span R s) = span R s (reiterated).

Русский

span R (span R s) = span R s (повторно).

LaTeX

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

Lean4

theorem span_singleton_smul_eq {r : R} (hr : IsUnit r) (x : M) : (R ∙ r • x) = R ∙ x :=
  by
  lift r to Rˣ using hr
  rw [← Units.smul_def]
  exact span_singleton_group_smul_eq R r x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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