dvd_prime

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.dvd_prime

English

For primes p and any m, m divides p if and only if m = 1 or m = p.

Русский

Для простого p и любого m верно: m делит p тогда и только тогда, когда m = 1 или m = p.

LaTeX

$$$ m \\mid p \\iff (m = 1) \\\\lor (m = p) $$$

Lean4

theorem dvd_prime {p m : ℕ+} (pp : p.Prime) : m ∣ p ↔ m = 1 ∨ m = p :=
  by
  rw [PNat.dvd_iff]
  rw [Nat.dvd_prime pp]
  simp

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

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

Разделы

Аффилиация

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