coprime_pow_left_iff — Mathlib

English

Let n>0. Then for all a,b, Coprime(a^n, b) ⇔ Coprime(a, b).

Русский

Пусть n>0. Тогда для любых a,b: Coprime(a^n, b) ⇔ Coprime(a, b).

LaTeX

$$$$\forall n>0\;\forall a,b \in \mathbb{N}, \mathrm{Coprime}(a^n, b) \iff \mathrm{Coprime}(a, b)$$$$

Lean4

@[simp]
theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) : Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b :=
  by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)
  rw [Nat.pow_succ, Nat.coprime_mul_iff_left]
  exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩

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