English
For a finite nonempty M, commProb(M) = 1 if and only if the operation on M is commutative (i.e., M is abelian).
Русский
Для конечной непустой M верность commProb(M) равна 1 тогда и только тогда, когда операция на M коммутирует (то есть M абелева).
LaTeX
$$commProb(M) = 1 \iff \text{Std.Commutative}((\cdot,\cdot): M \times M \to M)$$
Lean4
theorem commProb_eq_one_iff [h : Nonempty M] : commProb M = 1 ↔ Std.Commutative ((· * ·) : M → M → M) := by
classical
haveI := Fintype.ofFinite M
rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod, set_fintype_card_eq_univ_iff,
Set.eq_univ_iff_forall]
· exact ⟨fun h ↦ ⟨fun x y ↦ h (x, y)⟩, fun h x ↦ h.comm x.1 x.2⟩
· exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
