refactor(group_theory/commuting_probability): Use `finite` instead of `fintype` (#17397)
refactor(group_theory/commuting_probability): Use `finite` instead of `fintype` (#17397)

This PR refactors `group_theory/commuting_probability` to use `finite` instead of `fintype`.



Co-authored-by: Kyle Miller <04892e540c93233cb5dfa2674fa5218f82feced5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib