Conjugate_of_Set_with_Inverse_Closed_for_Inverses
Provedclosureconjugationgroup-theoryproofwiki
Let G be a group and S a subset. Let S_hat = S ∪ S⁻¹. Then the set of all conjugates of elements in S_hat is closed under inverses.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Conjugate_of_Set_with_Inverse_Closed_for_Inverses {G : Type _} [Group G] (S : Set G) : ∀ (a : G) (s : G), s ∈ S ∪ S⁻¹ → (a * s * a⁻¹)⁻¹ ∈ {a * t * a⁻¹ | (a : G) (t : G) (_ : t ∈ S ∪ S⁻¹)} := by sorrySource