pow

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.Coprime.pow

English

If m and n are coprime, then m^k and n^l are coprime for any k,l ∈ ℕ.

Русский

Если m и n взаимно простые, то m^k и n^l взаимно простые для любых k,l ∈ ℕ.

LaTeX

$$$ (gcd(m,n)=1) \rightarrow gcd(m^k, n^l)=1 $$$

Lean4

theorem pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k : ℕ).Coprime (n ^ l) := by rw [← coprime_coe] at *;
  apply Nat.Coprime.pow; apply h

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

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

Разделы

Аффилиация

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