coprime_pow_right_iff

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.coprime_pow_right_iff

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) : Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b := by
  rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru