mathlib

6a71007a - feat(group_theory/quotient_group) finiteness of groups for sequences of homomorphisms (#12660)