Commit 2022-11-08 14:54 072c8ce8

View on Github →

refactor(group_theory/commuting_probability): Use finite instead of fintype (#17397) This PR refactors group_theory/commuting_probability to use finite instead of fintype.

Estimated changes

Modified src/group_theory/commuting_probability.lean

modified theorem card_comm_eq_card_conj_classes_mul_card

modified def comm_prob

modified theorem comm_prob_def'

modified theorem comm_prob_def

modified theorem inv_card_commutator_le_comm_prob

modified theorem subgroup.comm_prob_quotient_le