prod_const_one — Mathlib

English

For any Finset s and commutative monoid M, the product of 1 over all elements of s is 1: ∏_{x ∈ s} 1 = 1.

Русский

Для любого конечного множества s и коммутативного моноида M произведение единицы по всем элементам s равно 1: ∏_{x ∈ s} 1 = 1.

LaTeX

$$$\\prod_{x \\in s} (1) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_const_one : (∏ _x ∈ s, (1 : M)) = 1 := by
  simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]

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