Set-like fintype

This file contains a fintype instance for set-like objects such as subgroups. If SetLike A B and Fintype B then Fintype A.

@[instance 100]

noncomputable instance SetLike.instFintype {A : Type u_1} {B : Type u_2} [SetLike A B] [Fintype B] : Fintype A

TODO: It should be possible to obtain a computable version of this for most SetLike objects. If we add those instances, we should remove this one.

Equations

• SetLike.instFintype = Fintype.ofInjective SetLike.coe ⋯

@[instance 100]

instance SetLike.instFinite {A : Type u_1} {B : Type u_2} [SetLike A B] [Finite B] : Finite A

Equations

• ⋯ = ⋯