English
The commuting probability of a direct product G × H equals the product of the commuting probabilities: commProb(G × H) = commProb(G) · commProb(H).
Русский
Вероятность коммутирования для прямого произведения групп равна произведению вероятностей коммутирования каждой группы: commProb(G × H) = commProb(G) · commProb(H).
LaTeX
$$commProb(G \times H) = commProb(G) \cdot commProb(H)$$
Lean4
theorem commProb_prod (M' : Type*) [Mul M'] : commProb (M × M') = commProb M * commProb M' :=
by
simp_rw [commProb_def, div_mul_div_comm, Nat.card_prod, Nat.cast_mul, mul_pow, ← Nat.cast_mul, ← Nat.card_prod,
Commute, SemiconjBy, Prod.ext_iff]
congr 2
exact
Nat.card_congr
⟨fun x => ⟨⟨⟨x.1.1.1, x.1.2.1⟩, x.2.1⟩, ⟨⟨x.1.1.2, x.1.2.2⟩, x.2.2⟩⟩, fun x =>
⟨⟨⟨x.1.1.1, x.2.1.1⟩, ⟨x.1.1.2, x.2.1.2⟩⟩, ⟨x.1.2, x.2.2⟩⟩, fun x => rfl, fun x => rfl⟩
