irreducible_iff — Mathlib

English

If p is associated to q, then p is irreducible if and only if q is irreducible.

Русский

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

LaTeX

$$$$\mathrm{Associated}(p,q) \Rightarrow (\mathrm{Irreducible}(p) \iff \mathrm{Irreducible}(q)).$$$$

Lean4

protected theorem irreducible_iff [Monoid M] {p q : M} (h : p ~ᵤ q) : Irreducible p ↔ Irreducible q :=
  ⟨h.irreducible, h.symm.irreducible⟩

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