prime_iff — Mathlib

English

If two elements p and q are associates, then p is prime if and only if q is prime.

Русский

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

LaTeX

$$$$\forall M \,[\mathrm{CommMonoidWithZero}\, M],\forall p,q \in M, p \sim_{\mathrm{a}} q \Rightarrow (\mathrm{Prime}(p) \iff \mathrm{Prime}(q)).$$$$

Lean4

theorem prime_iff [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) : Prime p ↔ Prime q :=
  ⟨h.prime, h.symm.prime⟩

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