mathlib3

d4343972 - feat(group_theory/conjugates) : define conjugates (#1029)

feat(group_theory/conjugates) : define conjugates (#1029) * feat(algebra/order_functions): generalize strict_mono.monotone (#1022) * moving stuff to where it belongs * removed unecessary import * Changed to union * Update src/group_theory/subgroup.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Stylistic changes * Added authorship * Moved mem_conjugates_of_set * Authorship * Trying fixes * Putting everything in the right order * removed import