smulRight_one_one

Mathlib.Topology.Algebra.Module.LinearMap

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

← MathLib Explorer

English

The map smulRight with the identity on the scalar side reduces to the original map c.

Русский

Осуществление smulRight с единицей сводит к исходной карте.

LaTeX

$$$\forall c, smulRight (1 : R_1 \to_L[R_1] R_1) (c 1) = c$.$$

Lean4

@[simp]
theorem smulRight_one_one (c : R₁ →L[R₁] M₂) : smulRight (1 : R₁ →L[R₁] R₁) (c 1) = c :=
  by
  ext
  simp [← ContinuousLinearMap.map_smul_of_tower]

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

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

Разделы

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

Аффилиация

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