op_mem_center_iff — Mathlib

English

Let M be a monoid. For every x in M, x is in the center of M if and only if op x is in the center of the opposite monoid M^{op}.

Русский

Пусть M — моноид. Для произвольного элемента x ∈ M правая часть: x лежит в центре M тогда и только тогда, когда образ x под операцией противоположного моноида, op x, лежит в центре M^{op}.

LaTeX

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

Lean4

@[to_additive]
theorem op_mem_center_iff [Mul M] {x : M} : op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M := by
  simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]; aesop

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