decidableMemCenter — Mathlib

English

There exists a decidable predicate for membership in the center when the ring is finite and has decidable equality.

Русский

Существует разрешимое по знаку членство в центре при конечном R и наличии разрешимого равенства.

LaTeX

$$$ \text{DecidablePred} (\,\cdot \in \mathrm{center}\, R\,)$ under finiteness and decidable equality.$$

Lean4

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

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