mathlib3

882fc132 - refactor(group_theory/finiteness): Make `group.rank` noncomputable (#16256)

refactor(group_theory/finiteness): Make `group.rank` noncomputable (#16256) I've been working on some more API for `group.rank`, and the decidability hypothesis was making lemma statements really clunky. If you wanted to say `group.rank G ≤ group.rank G'`, then the decidability hypotheses would add two lines to the statement of the lemma.