one_eq_span_one_set

Mathlib.Algebra.Algebra.Operations

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

English

The unit equals the span of the singleton {1} as a Submodule: (1 : Submodule R A) = span R {1}.

Русский

Единица равна span R {1} в контексте Submodule: (1 : Submodule R A) = span R {1}.

LaTeX

$$$ (1 : Submodule R A) = \\mathrm{span}_R\\{1\\} $$$

Lean4

theorem one_eq_span_one_set : (1 : Submodule R A) = span R 1 :=
  one_eq_span

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

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

Разделы

Аффилиация

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