decidableEq — Mathlib

English

Transfers DecidableEq across an equivalence: if β has DecidableEq, then α has DecidableEq.

Русский

Передача DecidableEq через эквивалентность: если у β есть DecidableEq, то и у α есть DecidableEq.

LaTeX

$$$\text{DecidableEq }\alpha \leftarrow\text{ via } e: \alpha \simeq \beta \text{ if } [DecidableEq \beta]$$$

Lean4

/-- Transfer `DecidableEq` across an equivalence. -/
protected def decidableEq (e : α ≃ β) [DecidableEq β] : DecidableEq α :=
  e.injective.decidableEq

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