decidableMemCenter — Mathlib

English

If R has decidable equality and is finite, then membership in the center is decidable.

Русский

Если R конечное кольцо с разрешимостью равенств, то принадлежность центра разрешима.

LaTeX

$$[DecidableEq R] [Fintype R] ⇒ DecidablePred (x ∈ center R)$$

Lean4

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

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