product_val

Mathlib.Data.Finset.Prod

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

English

The underlying multiset of the product s ×ˢ t is the product of the underlying multisets, i.e., the pair multiset equals the product multiset.

Русский

Базовый мультисет произведения равен произведению базовых мультисетов.

LaTeX

$$$(s \timesˢ t).1 = s.1 \timesˢ t.1$$$

Lean4

@[simp]
theorem product_val : (s ×ˢ t).1 = s.1 ×ˢ t.1 :=
  rfl

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

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

Разделы

Аффилиация

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