Set.center, Set.centralizer and the star operation #
theorem
Set.star_mem_center
{R : Type u_1}
[Mul R]
[StarMul R]
{a : R}
(ha : a ∈ Set.center R)
:
star a ∈ Set.center R
theorem
Set.star_mem_centralizer'
{R : Type u_1}
[Mul R]
[StarMul R]
{a : R}
{s : Set R}
(h : ∀ (a : R), a ∈ s → star a ∈ s)
(ha : a ∈ Set.centralizer s)
:
star a ∈ Set.centralizer s
theorem
Set.star_mem_centralizer
{R : Type u_1}
[Mul R]
[StarMul R]
{a : R}
{s : Set R}
(ha : a ∈ Set.centralizer (s ∪ star s))
:
star a ∈ Set.centralizer (s ∪ star s)