instDecidableEqFinpartition — Mathlib

English

If α has decidable equality, then Finpartition a has decidable equality as well.

Русский

Если у α есть разрешимое равенство, то и Finpartition a имеет разрешимое равенство.

LaTeX

$$$[DecidableEq \\alpha] \\Rightarrow DecidableEq(\\mathrm{Finpartition} a)$$$

Lean4

instance instDecidableEqFinpartition {α✝} {inst✝} {inst✝¹} {a✝} [DecidableEq✝ α✝] :
    DecidableEq✝ (@Finpartition✝ α✝ inst✝ inst✝¹ a✝) :=
  instDecidableEqFinpartition.decEq

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