smul_one_eq_span

Mathlib.Algebra.Algebra.Operations

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

← MathLib Explorer

English

For any x ∈ A, x • (1 : Submodule R A) = span R { x }.

Русский

Для любого x ∈ A верно x • (1) = span_R{ x }.

LaTeX

$$$ x \cdot (1 : Submodule R A) = \operatorname{span}{}_R\{ x \} $$$

Lean4

theorem smul_one_eq_span (x : A) : x • (1 : Submodule R A) = span R { x } := by
  rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]

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

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

Разделы

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

Аффилиация

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