Group_Example_x_inv_c_y
Provedexamples-of-groupsproofwiki
Given a group G and c ∈ G, the operation x * y = x ∘ c⁻¹ ∘ y defines a group structure on G.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Group_Example_x_inv_c_y {G : Type _} [Group G] (c : G) : ∀ x y : G, ∃ z : G, x * c⁻¹ * y = z := by sorrySource