English
Finite p₁-groups and p₂-groups with different primes p₁ ≠ p₂ have coprime orders.
Русский
Пусть конечные p₁-группы и p₂-группы имеют разные простые p₁ ≠ p₂; их порядки взаимно просты.
LaTeX
$$$\text{If } H_1 \text{ is a finite } p_1\text{-subgroup and } H_2 \text{ is a finite } p_2\text{-subgroup with } p_1 \neq p_2, \text{ then } \gcd(|H_1|,|H_2|)=1.$$$
Lean4
/-- finite p-groups with different p have coprime orders -/
theorem 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₂) [Finite H₁] [Finite H₂] (hH₁ : IsPGroup p₁ H₁)
(hH₂ : IsPGroup p₂ H₂) : Nat.Coprime (Nat.card H₁) (Nat.card H₂) :=
by
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
