CyclotomicInversion.lean

theorem map_eq_one_of_isConj_inv_of_coprime_two
    {G : Type u} {A : Type v} [Group G] [CommGroup A]
    (f : G →* A) {gamma : G} (hConj : IsConj gamma gamma⁻¹)
    (hCoprime : Nat.Coprime (orderOf (f gamma)) 2) :
    f gamma = 1

theorem map_eq_one_of_isConj_inv_of_odd_order
    {G : Type u} {A : Type v} [Group G] [CommGroup A]
    (f : G →* A) {gamma : G} (hConj : IsConj gamma gamma⁻¹)
    (hOdd : Odd (orderOf (f gamma))) :
    f gamma = 1

theorem map_eq_bot_of_forall_isConj_inv_of_card_coprime_two
    {G : Type u} {A : Type v} [Group G] [CommGroup A]
    (f : G →* A) (I : Subgroup G) [Finite I]
    (hConj : ∀ gamma : G, gamma ∈ I → IsConj gamma gamma⁻¹)
    (hCoprime : Nat.Coprime (Nat.card I) 2) :
    I.map f = ⊥

theorem subgroup_eq_bot_of_generator_isConj_inv_of_card_coprime_two
    {A : Type u} [CommGroup A] (I : Subgroup A) [Finite I]
    {gamma : A} (hGenerates : Subgroup.zpowers gamma = I)
    (hConj : IsConj gamma gamma⁻¹)
    (hCoprime : Nat.Coprime (Nat.card I) 2) :
    I = ⊥

theorem subgroup_eq_bot_of_card_coprime_every_prime
    {G : Type u} [Group G] (I : Subgroup G) [Finite I]
    (hCoprime : ∀ p : ℕ, p.Prime → Nat.Coprime (Nat.card I) p) :
    I = ⊥