chore(group_theory/*): Fix lint (#16095)
Fix the linting errors coming from `fintype_finite` and `to_additive_doc` in the `group_theory` folder (+ some in `data` and `combinatorics`). Remove the decidability assumptions to `decidable_powers`/`decidable_zpowers` because they are already noncomputable.
## Lemma renames
* `fintype` → `finite` in lemmas that used to assume `fintype` and now only assume `finite`
* `fintype.induction_empty_option'` → `fintype.induction_empty_option`
