noncommProd_empty

Mathlib.Data.Finset.NoncommProd

URI: https://scilib.ai/kg/mathlib#Multiset.noncommProd_empty

English

In a Monoid, the noncommProd of the empty multiset is the unit element, namely 1.

Русский

В моноиде некоммутативное произведение пустого мультисета равно единице.

LaTeX

$$$\\mathrm{noncommProd} (0:\\mathrm{Multiset} \\alpha) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem noncommProd_empty (h) : noncommProd (0 : Multiset α) h = 1 :=
  rfl

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

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

Разделы

Аффилиация

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