instDecidableEqComposition — Mathlib

English

There exists a decision procedure for equality on the set of compositions of n; i.e., the equality on Composition(n) is decidable.

Русский

Существет разрешимое равенство на множество композиции n; т.е. равенство на Composition(n) разрешимо.

LaTeX

$$$\\text{DecidableEq}(\\mathrm{Composition}(n))$$$

Lean4

instance instDecidableEqComposition {n✝} : DecidableEq✝ (@Composition✝ n✝) :=
  instDecidableEqComposition.decEq

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