Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.comm_prob_quotient_le

Modification history

2022-11-08 14:54
src/group_theory/commuting_probability.lean
refactor(group_theory/commuting_probability): Use `finite` instead of `fintype` (#17397) …
Modified subgroup.comm_prob_quotient_leView on Github →
2022-01-24 11:34
src/group_theory/commuting_probability.lean
feat(group_theory/commuting_probability): Commuting probability inequalities (#11564) …
Added subgroup.comm_prob_quotient_leView on Github →