coprime_or_dvd_of_prime

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.coprime_or_dvd_of_prime

English

For any prime p, and any i, either p ∤ i or p ∣ i.

Русский

Для любого простого p и любого i либо p не делит i, либо p делит i.

LaTeX

$$$$ \forall p,i \in \mathbb{N},\text{Prime}(p) \rightarrow (\gcd(p,i)=1 \lor p \mid i). $$$$

Lean4

theorem coprime_or_dvd_of_prime {p} (pp : Prime p) (i : ℕ) : Coprime p i ∨ p ∣ i := by rw [pp.dvd_iff_not_coprime];
  apply em

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

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

Разделы

Аффилиация

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