Mathlib.Algebra.Ring.Centralizer

Module docstring

{"# Centralizers of rings "}

Set.add_mem_centralizer theorem

[Distrib M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : a + b ∈ centralizer S

Full source

@[simp]
theorem add_mem_centralizer [Distrib M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
    a + b ∈ centralizer S := fun c hc => by rw [add_mul, mul_add, ha c hc, hb c hc]

Sum of Centralizing Elements is Centralizing

Informal description

Let $M$ be a type with a distributive structure. For any subset $S \subseteq M$ and elements $a, b \in M$ such that $a$ and $b$ commute with every element of $S$, their sum $a + b$ also commutes with every element of $S$.

Set.neg_mem_centralizer theorem

[Mul M] [HasDistribNeg M] (ha : a ∈ centralizer S) : -a ∈ centralizer S

Full source

@[simp]
theorem neg_mem_centralizer [Mul M] [HasDistribNeg M] (ha : a ∈ centralizer S) :
    -a ∈ centralizer S := fun c hc => by rw [mul_neg, ha c hc, neg_mul]

Negation Preserves Centralizer Membership in Magmas with Distributive Negation

Informal description

Let $M$ be a type with multiplication and distributive negation. For any subset $S \subseteq M$ and any element $a \in M$ that commutes with every element of $S$, the negation $-a$ also commutes with every element of $S$, i.e., $-a \in \text{centralizer}(S)$.