Fintype instance for Shrink

@[implicit_reducible]

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} α)

@[simp]

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