prod_zero

Mathlib.Data.PNat.Factors

URI: https://scilib.ai/kg/mathlib#PrimeMultiset.prod_zero

← MathLib Explorer

English

The product of the zero (empty) PrimeMultiset is the unit 1.

Русский

Произведение нулевого (пустого) PrimeMultiset равно единице.

LaTeX

$$$ (0 : \\text{PrimeMultiset}).prod = 1 $$$

Lean4

/-- The product map gives a homomorphism from the additive monoid
of multisets to the multiplicative monoid ℕ+. -/
theorem prod_zero : (0 : PrimeMultiset).prod = 1 := by exact Multiset.prod_zero

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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