unop_mem_center_iff — Mathlib

English

Let M be a monoid. For every x in M^{op}, unop x ∈ center(M) if and only if x ∈ center(M^{op}).

Русский

Пусть M — моноид. Для любого x ∈ M^{op} выполнено: unop x ∈ центр(M) тогда и только тогда, когда x ∈ центр(M^{op}).

LaTeX

$$$ \operatorname{unop} x \in \operatorname{center}(M) \iff x \in \operatorname{center}(M^{\mathrm{op}}) $$$

Lean4

@[to_additive]
theorem unop_mem_center_iff [Mul M] {x : Mᵐᵒᵖ} : unop x ∈ Set.center M ↔ x ∈ Set.center Mᵐᵒᵖ :=
  op_mem_center_iff.symm

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