prod_bool — Mathlib

English

Let α be a commutative monoid and f: Bool → α. Then the product over all booleans of f(b) equals f(true) · f(false).

Русский

Пусть α — коммутативный моноид и f: Bool → α. Тогда произведение по всем булевым значениям f(b) равно f(true) · f(false).

LaTeX

$$$\\prod_{b \\in \\{\\mathrm{true},\\mathrm{false}\\}} f(b) = f(\\mathrm{true})\\\\, f(\\mathrm{false})$$$

Lean4

@[to_additive]
theorem prod_bool [CommMonoid α] (f : Bool → α) : ∏ b, f b = f true * f false := by simp

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