dvd_or_dvd

Mathlib.Algebra.Prime.Defs

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

English

If a prime p divides a product a b, then p divides a or p divides b.

Русский

Если простая p делит произведение a b, то p делит a или p делит b.

LaTeX

$$p \mid a b \Rightarrow p \mid a \ \text{или}\ p \mid b$$

Lean4

theorem dvd_or_dvd {a b : M} (h : p ∣ a * b) : p ∣ a ∨ p ∣ b :=
  hp.2.2 a b h

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

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

Разделы

Аффилиация

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