@[simp]

theorem Fintype.card_multiplicative (α : Type u_1) [Fintype α] : Fintype.card (Multiplicative α) = Fintype.card α

@[simp]

theorem Fintype.card_additive (α : Type u_1) [Fintype α] : Fintype.card (Additive α) = Fintype.card α