mathlib3

a652850a - feat(algebra/group/type_tags): finite & infinite instances for additive/multiplicative group type tags (#16662)