mem_centralizer_iff — Mathlib

English

An element a belongs to the centralizer of s if and only if for all g in s, ag = ga and for all g in s, a g^* = g^* a.

Русский

Элемент a принадлежит централизатору s тогда и только тогда, когда для всех g∈s выполняется ag=ga и a g^*= g^* a.

LaTeX

$$$a \in \operatorname{centralizer}(R,s) \iff \forall g \in s,\ g a = a g \wedge (\star g) a = a (\star g)$$$

Lean4

theorem mem_centralizer_iff {s : Set A} {z : A} :
    z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g :=
  by
  change (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
  simp only [Set.mem_union, or_imp, forall_and, and_congr_right_iff]
  exact fun _ => ⟨fun hz a ha => hz _ (Set.star_mem_star.mpr ha), fun hz a ha => star_star a ▸ hz _ ha⟩

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