image_smul

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

The image of t under the map x ↦ a · x equals a · t; i.e., (a ·)'' t = a · t

Русский

Образ множества t под действием отображения x ↦ a · x равен a · t

LaTeX

$$$ (\\{ a \\cdot x \\mid x \\in t \\}) = a \\cdot t $$$

Lean4

@[to_additive]
theorem image_smul : (fun x ↦ a • x) '' t = a • t :=
  rfl

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

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

Разделы

Аффилиация

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