feat(algebra/group/type_tags): finite & infinite instances for additi…

…ve/multiplicative group type tags (#16662)

- adds finite & infinite instances for additive/multiplicative group type tags

src/algebra/group/type_tags.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import algebra.hom.group
 import logic.equiv.basic
+import data.finite.defs
 /-!
 # Type tags that turn additive structures into multiplicative, and vice versa
 
@@ -69,6 +70,12 @@ end multiplicative
 instance [inhabited α] : inhabited (additive α) := ⟨additive.of_mul default⟩
 instance [inhabited α] : inhabited (multiplicative α) := ⟨multiplicative.of_add default⟩
 
+instance [finite α] : finite (additive α) := finite.of_equiv α (by refl)
+instance [finite α] : finite (multiplicative α) := finite.of_equiv α (by refl)
+
+instance [infinite α] : infinite (additive α) := by tauto
+instance [infinite α] : infinite (multiplicative α) := by tauto
+
 instance [nontrivial α] : nontrivial (additive α) :=
 additive.of_mul.injective.nontrivial