English
For a finite index set α and i : α → Type with multiplication, the commuting probability of the dependent product equals the product over α of the commuting probabilities.
Русский
Для конечного множества индексов α и i: α → Type с умножением, комм Prob зависимого произведения равна произведению вероятностей по каждому индексу.
LaTeX
$$commProb(∀ a, i(a)) = \prod_{a} commProb(i(a))$$
Lean4
theorem commProb_pi {α : Type*} (i : α → Type*) [Fintype α] [∀ a, Mul (i a)] :
commProb (∀ a, i a) = ∏ a, commProb (i a) :=
by
simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod, ← Nat.card_pi, Commute, SemiconjBy,
funext_iff]
congr 2
exact
Nat.card_congr
⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1, fun a => (x a).1.2⟩, fun a => (x a).2⟩,
fun x => rfl, fun x => rfl⟩
