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

source
instance instFiniteAdditive {α : Type u} [Finite α] :
Finite (Additive α)
source
instance instFiniteMultiplicative {α : Type u} [Finite α] :
Finite (Multiplicative α)
source
instance instInfiniteAdditive {α : Type u} [h : Infinite α] :
Infinite (Additive α)
source
instance instInfiniteMultiplicative {α : Type u} [h : Infinite α] :
Infinite (Multiplicative α)
source
instance Additive.fintype {α : Type u} [Fintype α] :
Fintype (Additive α)
Equations

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

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

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

source
@[simp]
theorem Fintype.card_multiplicative (α : Type u_1) [Fintype α] :
card (Multiplicative α) = card α
source
@[simp]
theorem Fintype.card_additive (α : Type u_1) [Fintype α] :
card (Additive α) = card α