irreducible_iff — Mathlib

English

Irreducible p ⇔ (¬IsUnit p) ∧ ∀ a,b, p = a*b → IsUnit a ∨ IsUnit b.

Русский

Неразложимый p эквивалентно: не единица и для любых a,b, p = a b → IsUnit a ∨ IsUnit b.

LaTeX

$$$\\text{Irreducible } p \\Leftrightarrow (\\neg IsUnit\\ p) \\land \\forall\\{a,b\\},\\ p = a b \\Rightarrow IsUnit\\ a \\lor IsUnit\\ b$$$

Lean4

@[to_additive]
theorem irreducible_iff : Irreducible p ↔ ¬IsUnit p ∧ ∀ ⦃a b⦄, p = a * b → IsUnit a ∨ IsUnit b
    where
  mp hp := ⟨hp.not_isUnit, hp.isUnit_or_isUnit⟩
  mpr hp := ⟨hp.1, hp.2⟩

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