mul_def

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The product s * t is defined as the image of s × t under the map (x,y) ↦ x*y.

Русский

Произведение s * t задано образом image (s × t) через отображение (x,y) ↦ x*y.

LaTeX

$$$s * t = (s \timesˢ t).image (fun p : \alpha × \alpha => p.1 * p.2)$$$

Lean4

@[to_additive]
theorem mul_def : s * t = (s ×ˢ t).image fun p : α × α => p.1 * p.2 :=
  rfl

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

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

Разделы

Аффилиация

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