Opposite_Group_is_Group
Provedopposite-groupsproofwiki
The opposite group (with reversed multiplication) of a group is also a group.
Preamble
import Mathlib.Algebra.Group.Opposite
Formal statement
theorem Opposite_Group_is_Group {G : Type _} [Group G] (a b c : MulOpposite G) : a * b * c = a * (b * c) := by sorrySource