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.
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 (_ : Function.Injective SetLike.coe)