image_mul_product

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The image of the pairwise product map equals the pointwise product: ((s ×ˢ t).image (x.fst * x.snd)) = s * t.

Русский

Изображение отображения пара x ∈ s, y ∈ t ↦ x*y равно произведению s и t.

LaTeX

$$$((s \timesˢ t).image (fun x : α × α => x.fst * x.snd)) = s * t$$$

Lean4

@[to_additive]
theorem image_mul_product : ((s ×ˢ t).image fun x : α × α => x.fst * x.snd) = s * t :=
  rfl

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

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

Разделы

Аффилиация

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