Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.comm_prob_subgroup_le

Modification history

2022-01-24 11:34
src/group_theory/commuting_probability.lean
feat(group_theory/commuting_probability): Commuting probability inequalities (#11564) …
Added subgroup.comm_prob_subgroup_leView on Github →