dvd_pow

Mathlib.RingTheory.Int.Basic

URI: https://scilib.ai/kg/mathlib#Int.Prime.dvd_pow

← MathLib Explorer

English

If p is prime and p divides n^k, then p divides n (in integers).

Русский

Если p — простое и делит p | n^k, то p делит n (в целых числах).

LaTeX

$$$p\\text{ prime} \\land p \\mid n^k \\Rightarrow p \\mid n.$$$

Lean4

theorem dvd_pow {n : ℤ} {k p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ n ^ k) : p ∣ n.natAbs :=
  by
  rw [Int.natCast_dvd, Int.natAbs_pow] at h
  exact hp.dvd_of_dvd_pow h

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

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

Разделы

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

Аффилиация

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