decidableMemCenter — Mathlib

English

The center acts commutatively on the monoid; smul by a center element commutes with any element.

Русский

Центр действует на моноид коммутативно: умножение элемента центра на элемент коммутирует с любым элементом.

LaTeX

$$∀ m ∈ center M, ∀ x ∈ M, m x = x m$$

Lean4

@[to_additive]
instance decidableMemCenter (a) [Decidable <| ∀ b : M, b * a = a * b] : Decidable (a ∈ center M) :=
  decidable_of_iff' _ mem_center_iff

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