smul_set_range

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

a • range f = range (i ↦ a • f i)

Русский

a • range f = range (i ↦ a • f i)

LaTeX

$$$ a \\cdot \\mathrm{range}\\, f = \\mathrm{range}\\, (\\lambda i. a \\cdot f i) $$$

Lean4

@[to_additive]
theorem smul_set_range [SMul α β] {ι : Sort*} (a : α) (f : ι → β) : a • range f = range fun i ↦ a • f i :=
  (range_comp ..).symm

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

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

Разделы

Аффилиация

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