dvd_pow'

Mathlib.RingTheory.Int.Basic

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

← MathLib Explorer

English

Let p be a prime and p divides n^k in ℤ. Then p divides n.

Русский

Пусть 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 :=
  by
  rw [Int.natCast_dvd]
  exact Int.Prime.dvd_pow hp h

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

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

Разделы

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

Аффилиация

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