apply_mem_center_iff — Mathlib

English

An element maps to the center under e iff its preimage is central under the inverse.

Русский

Элемент принадлежит центру после применения e тогда и только тогда, когда его предобраз в M центральен после применения обратного e.

LaTeX

$$e x ∈ center N ↔ x ∈ center M$$

Lean4

@[to_additive]
theorem _root_.MulEquivClass.apply_mem_center_iff {F} [EquivLike F M N] [Mul M] [Mul N] [MulEquivClass F M N] (e : F)
    {x : M} : e x ∈ Set.center N ↔ x ∈ Set.center M :=
  ⟨(by simpa using MulEquivClass.apply_mem_center (MulEquivClass.toMulEquiv e).symm ·),
    MulEquivClass.apply_mem_center e⟩

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