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 : ∀ (a : R), a sstar a s) (ha : 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)) :