dvd_of_dvd_pow

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Prime.dvd_of_dvd_pow

English

If p is prime and p ∣ m^n, then p ∣ m.

Русский

Пусть p — простое число и p делит m^n; тогда p делит m.

LaTeX

$$$$ \forall p,m,n \in \mathbb{N},\ ext{Prime}(p) \rightarrow p \mid m^n \rightarrow p \mid m. $$$$

Lean4

theorem dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m ^ n) : p ∣ m :=
  pp.prime.dvd_of_dvd_pow h

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

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

Разделы

Аффилиация

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