dvd_pow_iff_dvd

Mathlib.Algebra.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Prime.dvd_pow_iff_dvd

English

For n ≠ 0, p divides a^n iff p divides a.

Русский

Для n ≠ 0, p делит a^n тогда и только тогда, когда p делит a.

LaTeX

$$p \mid a^{n} \iff p \mid a , \quad n \neq 0$$

Lean4

theorem dvd_pow_iff_dvd {a : M} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ n ↔ p ∣ a :=
  ⟨hp.dvd_of_dvd_pow, (dvd_pow · hn)⟩

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

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

Разделы

Аффилиация

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