Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 14:24 22311732

View on Github →

feat(group_theory/commuting_probability): New file (#11243) This PR introduces commuting probabilities of finite groups.

Estimated changes

added def comm_prob
added theorem comm_prob_def'
added theorem comm_prob_def
added theorem comm_prob_eq_one_iff
added theorem comm_prob_le_one
added theorem comm_prob_pos