associated_of_dvd — Mathlib

English

If p and q are prime and p divides q, then p is associated to q.

Русский

Если p и q — простые и p делит q, тогда p ассоциировано с q.

LaTeX

$$$ [CancelCommMonoidWithZero M] {p q : M} (p_prime : Prime p) (q_prime : Prime q) (dvd : p \mid q) : Associated p q $$$

Lean4

theorem associated_of_dvd [CancelCommMonoidWithZero M] {p q : M} (p_prime : Prime p) (q_prime : Prime q) (dvd : p ∣ q) :
    Associated p q :=
  p_prime.irreducible.associated_of_dvd q_prime.irreducible dvd

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