decidableMemCenter — Mathlib

English

If R is a finite-type nonunital ring with decidable equality, then membership in the center is decidable; i.e., for every z in R, the statement z ∈ center(R) is decidable.

Русский

Если R — конечное по типу кольцо без единицы с разрешимостью сравнения, то принадлежность элемента центру решаема: для каждого z ∈ R выражение z ∈ center(R) разрешимо.

LaTeX

$$$\\forall z:\\,R,\\ \\mathsf{Decidable}(z \\in \\mathrm{center}(R))$$$

Lean4

instance decidableMemCenter [DecidableEq R] [Fintype R] : DecidablePred (· ∈ center R) := fun _ =>
  decidable_of_iff' _ mem_center_iff

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