decidableEqEquivFintype — Mathlib

English

There is a decidable equality on the type α ↪ β provided [DecidableEq β] and [Fintype α].

Русский

Существует разрешимое равенство на множества вложений α ↪ β при данных [DecidableEq β] и [Fintype α].

LaTeX

$$$$ \text{DecidableEq}(\alpha \hookrightarrow \beta) $$$$

Lean4

instance decidableEqEquivFintype [DecidableEq β] [Fintype α] : DecidableEq (α ≃ β) := fun a b =>
  decidable_of_iff (a.1 = b.1) Equiv.coe_fn_injective.eq_iff

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