English
If p and p' are distinct primes, then the p-primary component and the p'-primary component are disjoint; their intersection is the trivial submonoid (containing only the identity).
Русский
Если p и p' — различные простые числа, то p-первичный компонент и p'-первичный компонент не пересекаются; их пересечение тривиально и состоит только из единицы.
LaTeX
$$$\forall p',\; \text{Prime}(p'),\; p \neq p'\;\Rightarrow\; \text{Disjoint}(CommMonoid.primaryComponent\,G\,p,\ CommMonoid.primaryComponent\,G\,p').$$$
Lean4
/-- The `p`- and `q`-primary components are disjoint for `p ≠ q`. -/
@[to_additive /-- The `p`- and `q`-primary components are disjoint for `p ≠ q`. -/
]
theorem disjoint {p' : ℕ} [hp' : Fact p'.Prime] (hne : p ≠ p') :
Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p') :=
Submonoid.disjoint_def.mpr <| by
rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩
· rwa [pow_zero, orderOf_eq_one_iff] at hn
· exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne
