Set-like fintype #
This file contains a fintype instance for set-like objects such as subgroups. If set_like A B
and fintype B then fintype A.
@[protected, nolint, instance]
noncomputable
def
set_like.fintype
{A : Type u_1}
{B : Type u_2}
[fintype B]
[set_like A B] :
fintype A
TODO: It should be possible to obtain a computable version of this for most set_like objects. If we add those instances, we should remove this one.