Conjugating idempotents

If b * a = 1 in a monoid, then a * e * b is idempotent whenever e is. In particular, conjugating an idempotent by a unit gives an idempotent, as does conjugating by a one-sided inverse pair such as 1 + N and 1 - N for a square-zero element N of a ring.

theorem IsIdempotentElem.mul_mul_of_mul_eq_one {M : Type u_1} [Monoid M] {e a b : M} (he : IsIdempotentElem e) (h : b * a = 1) : IsIdempotentElem (a * e * b)

If b * a = 1, then a * e * b is idempotent whenever e is.