Element_of_Group_Not_Conjugate_to_Proper_Subgroup
Provedconjugationgroup-theoryproofwikiproper-subgroup
In a finite group G, if H is a proper subgroup, then there exists at least one element not conjugate to any element of H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Element_of_Group_Not_Conjugate_to_Proper_Subgroup {G : Type _} [Group G] [Fintype G] (H : Subgroup G) (hH : H ≠ ⊤) : ∃ g : G, ∀ a : G, a * g * a⁻¹ ∉ (H : Set G) := by sorrySource