mathlib

999e0925 - feat(group_theory/finiteness): Add variants of `rank_closure_le_card` (#16364)

feat(group_theory/finiteness): Add variants of `rank_closure_le_card` (#16364) This PR adds some more API lemmas for `group.rank`. `rank_congr` is useful since `rw h` and `simp only [h]` have run into trouble.