toSpanSingleton_apply

Mathlib.Topology.Algebra.Module.LinearMap

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

English

The action of toSpanSingleton on r is r • x.

Русский

Действие toSpanSingleton на r равно r • x.

LaTeX

$$$ toSpanSingleton(R_1, x)(r) = r \cdot x$.$$

Lean4

@[simp]
theorem toSpanSingleton_apply (x : M₁) (r : R₁) : toSpanSingleton R₁ x r = r • x :=
  rfl

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

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

Разделы

Аффилиация

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