Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inv_card_commutator_le_comm_prob

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 inv_card_commutator_le_comm_probView on Github →
2022-01-24 11:34
src/group_theory/commuting_probability.lean
feat(group_theory/commuting_probability): Commuting probability inequalities (#11564) …
Added inv_card_commutator_le_comm_probView on Github →