English
Two p-subgroups of a group G with distinct primes p₁ ≠ p₂ intersect trivially: H₁ ∩ H₂ = {e}.
Русский
Две p-подгруппы \(H_1\) и \(H_2\) в группе \(G\) при отличных p-значениях \(p_1 \neq p_2\) пересекаются тривиально: \(H_1 \cap H_2 = \\{e\\}\).
LaTeX
$$$\\text{If } p_1 \\neq p_2 \\text{ are primes and } H_1, H_2 \\le G \\text{ with } H_1 \\text{ a } p_1\\text{-subgroup}, H_2 \\text{ a } p_2\\text{-subgroup}, \\text{ then } H_1 \\cap H_2 = \\{e\\}.$$$
Lean4
/-- p-groups with different p are disjoint -/
theorem disjoint_of_ne (p₁ p₂ : ℕ) [hp₁ : Fact p₁.Prime] [hp₂ : Fact p₂.Prime] (hne : p₁ ≠ p₂) (H₁ H₂ : Subgroup G)
(hH₁ : IsPGroup p₁ H₁) (hH₂ : IsPGroup p₂ H₂) : Disjoint H₁ H₂ :=
by
rw [Subgroup.disjoint_def]
intro x hx₁ hx₂
obtain ⟨n₁, hn₁⟩ := iff_orderOf.mp hH₁ ⟨x, hx₁⟩
obtain ⟨n₂, hn₂⟩ := iff_orderOf.mp hH₂ ⟨x, hx₂⟩
rw [Subgroup.orderOf_mk] at hn₁ hn₂
have : p₁ ^ n₁ = p₂ ^ n₂ := by rw [← hn₁, ← hn₂]
rcases n₁.eq_zero_or_pos with (rfl | hn₁)
· simpa using hn₁
· exact absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne
