Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 11:34 ed903019

View on Github →

feat(group_theory/commuting_probability): Commuting probability inequalities (#11564) This PR adds some inequalities for the commuting probability.

Estimated changes