commProb_function — Mathlib

English

For i : α → Type with multiplicative structure, the commuting probability of the dependent product equals the product over α of the commuting probabilities.

Русский

Для i : α → Type с умножением, комм Prob зависимого произведения равна произведению комм Prob каждого i(a).

LaTeX

$$commProb(∀ a, i(a)) = \prod_{a} commProb(i(a))$$

Lean4

theorem commProb_function {α β : Type*} [Fintype α] [Mul β] : commProb (α → β) = (commProb β) ^ Fintype.card α := by
  rw [commProb_pi, Finset.prod_const, Finset.card_univ]

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