Commit 2022-09-03 10:46 882fc132

View on Github →

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.

Estimated changes

Modified src/group_theory/finiteness.lean

deleted def group.rank

modified theorem group.rank_le

modified theorem group.rank_spec

Modified src/group_theory/schreier.lean

modified theorem subgroup.rank_le_index_mul_rank