star_mem_centralizer' — Mathlib

English

If a subset s is closed under star and a lies in the centralizer of s, then star a lies in the centralizer of s.

Русский

Если множество s замкнуто относительно операции звезды и элемент a коммутирует со всеми элементами из s, то и star a коммутирует со всеми элементами из s.

LaTeX

$$$\\Big( \\forall x \\in s, \\ star\\ x \\in s \\Big) \\land \\Big( a \\in \\mathrm{centralizer}(s) \\Big) \\Rightarrow \\ star\\ a \\in \\mathrm{centralizer}(s)$$$

Lean4

theorem star_mem_centralizer' (h : ∀ a : R, a ∈ s → star a ∈ s) (ha : a ∈ Set.centralizer s) :
    star a ∈ Set.centralizer s := fun y hy => by simpa using congr_arg star (ha _ (h _ hy)).symm

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