Fintype instance for Shrink

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

Equations

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

@[simp]

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