mathlib3
443c02be - feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363)

Commit

3 years ago

feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363) This PR adds some more API lemmas for `group.rank`.

Author

tb65536

Parents

f46fcef9

mathlib3 443c02be - feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363)

mathlib3
443c02be - feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363)