coprime_pow_primes — Mathlib

English

If p and q are primes with p ≠ q, then p^n and q^m are coprime.

Русский

Если p и q — простые числа, p ≠ q, то p^n и q^m взаимно просты.

LaTeX

$$$$ \forall p,q,n,m \in \mathbb{N},\ \text{Prime}(p) \land \text{Prime}(q) \land p \neq q \Rightarrow \gcd(p^n, q^m) = 1. $$$$

Lean4

theorem coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : Prime p) (pq : Prime q) (h : p ≠ q) : Coprime (p ^ n) (q ^ m) :=
  ((coprime_primes pp pq).2 h).pow _ _

Похожие утверждения