English
For any n and list l, the commuting probability of the product n :: l equals the product of the commuting probability of the head DihedralGroup(n) and the commuting probability of the product l.
Русский
Для любого n и списка l вероятность коммутирования произведения n :: l равна произведению вероятности коммутирования диагедральной группы DihedralGroup(n) и вероятности коммутирования Product(l).
LaTeX
$$$ \operatorname{commProb}( \operatorname{Product}(n :: l)) = \operatorname{commProb}( \mathrm{DihedralGroup}(n)) \cdot \operatorname{commProb}( \operatorname{Product}(l)). $$$
Lean4
theorem commProb_cons (n : ℕ) (l : List ℕ) :
commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l) := by
simp only [commProb_pi, Fin.prod_univ_succ, Fin.getElem_fin, Fin.val_succ, Fin.val_zero, List.getElem_cons_zero,
List.length_cons, List.getElem_cons_succ]
