image_smul

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.image_smul

English

The image under the scalar action commutes with the scalar action: s.image (a • ·) = a • s.

Русский

Образ при действии скаляра коммутирует: s.image (a • ·) = a • s.

LaTeX

$$$s.\operatorname{image}(a \cdot \cdot) = a \cdot s$$$

Lean4

@[to_additive]
theorem image_smul : s.image (a • ·) = a • s :=
  rfl

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

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

Разделы

Аффилиация

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