We prove that centralizer and set_centralilzer are submonoid/subgroups/subrings depending on the available structures, and provide operations on commute _ _.
E.g., if a, b, and c are elements of a semiring, and that hb : commute a b and hc : commute a c. Then hb.pow_left 5 proves commute (a ^ 5) b and (hb.pow_right 2).add_right (hb.mul_right hc) proves commute a (b ^ 2 + b * c).
Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like rw [(hb.pow_left 5).eq] rather than just rw [hb.pow_left 5].
Most of the proofs come from the properties of semiconj_by.
Two elements commute, if a * b = b * a.
Equality behind commute a b; useful for rewriting.
Any element commutes with itself.
If a commutes with b, then b commutes with a.
If a commutes with both b and c, then it commutes with their product.
If both a and b commute with c, then their product commutes with c.
Centralizer of an element a : S is the set of elements that commute with a.
Centralizer of a set T is the set of elements that commute with all a ∈ T.