mathlib

08977be6 - feat(algebra/semiconj): define `semiconj_by` and some operations (#1576)

feat(algebra/semiconj): define `semiconj_by` and some operations (#1576) * feat(algebra/semiconj): define `semiconj_by` and some operations Also rewrite `algebra/commute` to reuse results from `algebra/semiconj`. * Some `@[simp]` attributes * Fixes by @rwbarton, more docs * Add two more constructors