mathlib documentation

data.set_like.fintype

Set-like fintype #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[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.

Equations
source
@[protected, nolint, instance]
def set_like.finite {A : Type u_1} {B : Type u_2} [finite B] [set_like A B] :
finite A