Finite, Infinite and Fintype are preserved by Additive and Multiplicative.

instance instFiniteAdditive {α : Type u} [Finite α] : Finite (Additive α)

instance instFiniteMultiplicative {α : Type u} [Finite α] : Finite (Multiplicative α)

instance instInfiniteAdditive {α : Type u} [h : Infinite α] : Infinite (Additive α)

instance instInfiniteMultiplicative {α : Type u} [h : Infinite α] : Infinite (Multiplicative α)

instance Additive.fintype {α : Type u} [Fintype α] : Fintype (Additive α)

Equations

• Additive.fintype = Fintype.ofEquiv α Additive.ofMul

instance Multiplicative.fintype {α : Type u} [Fintype α] : Fintype (Multiplicative α)

Equations

• Multiplicative.fintype = Fintype.ofEquiv α Multiplicative.ofAdd

@[simp]

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

@[simp]

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