Documentation

Mathlib.Algebra.Star.Center

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) :
theorem Set.star_mem_centralizer' {R : Type u_1} [Mul R] [StarMul R] {a : R} {s : Set R} (h : as, star a s) (ha : a s.centralizer) :
star a s.centralizer
theorem Set.star_mem_centralizer {R : Type u_1} [Mul R] [StarMul R] {a : R} {s : Set R} (ha : a (s star s).centralizer) :
star a (s star s).centralizer