prime_dvd_prime_iff_eq — Mathlib

English

In a cancellative commutative monoid with zero and with subsingleton units, for primes p and q, p divides q if and only if p equals q.

Русский

В моноиде c нулём, с единицами, образующими подмножество, простые p,q: p делит q тогда и только если p = q.

LaTeX

$$$$\forall p,q \in M,\ \mathrm{Prime}(p) \land \mathrm{Prime}(q) \Rightarrow p \mid q \iff p = q.$$$$

Lean4

theorem prime_dvd_prime_iff_eq {M : Type*} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p q : M} (pp : Prime p)
    (qp : Prime q) : p ∣ q ↔ p = q := by rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]

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