mem_centralizer_iff — Mathlib

English

Characterization of membership in centralizer: an element z belongs to centralizer R s if and only if for every g ∈ s, g z = z g and star g z = z star g.

Русский

Членство в централизатoре описывается так: z ∈ centralizer R s ⇔ ∀ g ∈ s, g z = z g и star g z = z star g.

LaTeX

$$$z \\in centralizer\\ R\\ s \\iff \\forall g \\in s, g z = z g \\wedge star\\ g z = z \\ star g$$$

Lean4

nonrec 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
  simp [← SetLike.mem_coe, centralizer_union, ← image_star, mem_centralizer_iff, forall_and]

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