Commit 2022-03-04 09:26 052d027f

refactor(algebra/category/Group/basic): Avoid data shuffle in mul_equiv.to_Group_iso (#12407) Change the definition of mul_equiv.to_Group_iso from {X Y : Type*} [group X] [group Y] (e : X ≃* Y) : Group.of X ≅ Group.of Y to {X Y : Group} (e : X ≃* Y) : X ≅ Y. Not making X and Y into Groups on the fly avoids rebundling them when they already are Groups, which breaks definitional equality.