dvd_prime_iff_associated — Mathlib

English

Let M be a cancellative commutative monoid with zero. For primes p and q in M, p divides q if and only if p and q are associated.

Русский

Пусть M — CancelCommMonoidWithZero. Пусть p и q — простые элементы M. Тогда p делит q тогда и только если p и q ассоциированы.

LaTeX

$$$$\forall M \, [\mathrm{CancelCommMonoidWithZero}\, M],\\ \forall p,q \in M, (\mathrm{Prime}(p) \land \mathrm{Prime}(q)) \Rightarrow p \mid q \iff \mathrm{Associated}(p,q).$$$$

Lean4

theorem dvd_prime_iff_associated [CancelCommMonoidWithZero M] {p q : M} (pp : Prime p) (qp : Prime q) :
    p ∣ q ↔ Associated p q :=
  pp.irreducible.dvd_irreducible_iff_associated qp.irreducible

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