coe_smul

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#AddGroupSeminorm.coe_smul

English

The smul operation on AddGroupSeminorm respects the scalar action on the underlying Real/NNReal structure; (r • p) x = r • p x.

Русский

Умножение AddGroupSeminorm взаимодействует с действием над R; (r • p) x = r • p x.

LaTeX

$$$ (r \cdot p)(x) = r \cdot p(x) $$$

Lean4

@[simp, norm_cast]
theorem coe_smul (r : R) (p : AddGroupSeminorm E) : ⇑(r • p) = r • ⇑p :=
  rfl

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

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

Разделы

Аффилиация

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