toSpanSingleton_one

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.toSpanSingleton_one

English

toSpanSingleton preserves addition: it is additive.

Русский

toSpanSingleton сохраняет сложение: отображение аддитивно.

LaTeX

$$$\text{toSpanSingleton}(R_1)(x+y) = \text{toSpanSingleton}(R_1)x + \text{toSpanSingleton}(R_1)y$.$$

Lean4

theorem toSpanSingleton_one (x : M₁) : toSpanSingleton R₁ x 1 = x :=
  one_smul _ _

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

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

Разделы

Аффилиация

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