mathlib

a29bd58d - feat(algebra/regular/basic): add lemma commute.is_regular_iff (#13104)

feat(algebra/regular/basic): add lemma commute.is_regular_iff (#13104) This lemma shows that an element that commutes with every element is regular if and only if it is left regular.