English
There is a DecidableEq instance for the i-th function type of the sum language, provided a DecidableEq instance on the corresponding component function type.
Русский
Существуют инстансы DecidableEq для функции i-й арности в суммарном языке, при условии наличия DecidableEq для соответствующей компоненты.
LaTeX
$$$DecidableEq((\langle f,R \rangle : Language).Functions(i))$$$
Lean4
/-- Passes a `DecidableEq` instance on a type of function symbols through the `Language`
constructor. Despite the fact that this is proven by `inferInstance`, it is still needed -
see the `example`s in `ModelTheory/Ring/Basic`. -/
instance instDecidableEqFunctions {f : ℕ → Type*} {R : ℕ → Type*} (n : ℕ) [DecidableEq (f n)] :
DecidableEq ((⟨f, R⟩ : Language).Functions n) :=
inferInstance
