From d6c002c7fd7386a52be1a5a1b23250e9fd5d1c16 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 2 Feb 2022 14:51:44 +0000 Subject: [PATCH] feat(group_theory/p_group): finite p-groups with different p have coprime orders (#11775) --- src/group_theory/p_group.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/group_theory/p_group.lean b/src/group_theory/p_group.lean index bdc2a2b838d72..4e3626f288d65 100644 --- a/src/group_theory/p_group.lean +++ b/src/group_theory/p_group.lean @@ -248,6 +248,18 @@ lemma to_sup_of_normal_left' {H K : subgroup G} (hH : is_p_group p H) (hK : is_p (hHK : K ≤ H.normalizer) : is_p_group p (H ⊔ K : subgroup G) := (congr_arg (λ H : subgroup G, is_p_group p H) sup_comm).mp (to_sup_of_normal_right' hK hH hHK) +/-- finite p-groups with different p have coprime orders -/ +lemma coprime_card_of_ne {G₂ : Type*} [group G₂] + (p₁ p₂ : ℕ) [hp₁ : fact p₁.prime] [hp₂ : fact p₂.prime] (hne : p₁ ≠ p₂) + (H₁ : subgroup G) (H₂ : subgroup G₂) [fintype H₁] [fintype H₂] + (hH₁ : is_p_group p₁ H₁) (hH₂ : is_p_group p₂ H₂) : + nat.coprime (fintype.card H₁) (fintype.card H₂) := +begin + obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁, rw heq₁, clear heq₁, + obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂, rw heq₂, clear heq₂, + exact nat.coprime_pow_primes _ _ (hp₁.elim) (hp₂.elim) hne, +end + /-- p-groups with different p are disjoint -/ lemma disjoint_of_ne (p₁ p₂ : ℕ) [hp₁ : fact p₁.prime] [hp₂ : fact p₂.prime] (hne : p₁ ≠ p₂) (H₁ H₂ : subgroup G) (hH₁ : is_p_group p₁ H₁) (hH₂ : is_p_group p₂ H₂) :