instDecidableEq — Mathlib

English

If R has decidable equality, then UnifEigenvalues(f,k) also has decidable equality.

Русский

Если равенство в R разрешимо, то и равенство в множестве UnifEigenvalues(f,k) разрешимо.

LaTeX

$$DecidableEq (UnifEigenvalues f k)$$

Lean4

instance instDecidableEq [DecidableEq R] (f : Module.End R M) (k : ℕ∞) : DecidableEq (UnifEigenvalues f k) :=
  inferInstanceAs (DecidableEq (Subtype (fun x : R ↦ f.HasUnifEigenvalue x k)))

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