Fintype instance for Shrink

noncomputable instance Shrink.instFintype {α : Type u} [Fintype α] : Fintype (Shrink.{v, u} α)

Equations

• Shrink.instFintype = Fintype.ofEquiv α (equivShrink α)

instance Shrink.instFinite {α : Type u} [Finite α] : Finite (Shrink.{v, u} α)

Equations

• ⋯ = ⋯

@[simp]

theorem Fintype.card_shrink {α : Type u} [Fintype α] [Fintype (Shrink.{v, u} α)] : Fintype.card (Shrink.{v, u} α) = Fintype.card α