of_fintype — Mathlib

English

If α is a fintype, then α is finite (the underlying finiteness is automatic from the fintype structure).

Русский

Если α — конечный тип, то α конечен (мощность фиксирована структурой конечного типа).

LaTeX

$$$\text{Finite}(\alpha) \text{ follows from } [\text{Fintype }\alpha].$$$

Lean4

/-- For efficiency reasons, we want `Finite` instances to have higher
priority than ones coming from `Fintype` instances. -/
instance (priority := 900) of_fintype (α : Type*) [Fintype α] : Finite α :=
  Fintype.finite ‹_›

Похожие утверждения