Theorems · Definition · combinatorics

FunLike.fintype

(G : Type u_2) →
  {α : Type u_3} → {γ : Type u_4} → [FunLike G α γ] → [DecidableEq α] → [Fintype α] → [Fintype γ] → Fintype G

All FunLikes are finite if their domain and codomain are. Non-dependent version of DFunLike.fintype that might be easier to infer. This is not an instance because specific FunLike types might have a better-suited definition.

Defined in: Mathlib.Data.FunLike.Fintype
Cited by: 0 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: FunLike DecidableEq Fintype Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fintypestatement and proof · cited by 7,736
FunLikestatement and proof · cited by 2,560
DFunLike.fintypeproof · cited by 0

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.