dvd_or_isRelPrime

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Irreducible.dvd_or_isRelPrime

← MathLib Explorer

English

For an irreducible p, either p divides n or p is relatively prime to n.

Русский

Для неприводимого p либо p делит n, либо p относительно просто к n.

LaTeX

$$$$\mathrm{Irreducible}(p) \Rightarrow p \mid n \lor \mathrm{IsRelPrime}(p,n).$$$$

Lean4

theorem dvd_or_isRelPrime [Monoid M] {p n : M} (hp : Irreducible p) : p ∣ n ∨ IsRelPrime p n :=
  Classical.or_iff_not_imp_left.mpr hp.isRelPrime_iff_not_dvd.2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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