reducible_notMem_factorSet — Mathlib

English

If p is not irreducible (i.e., reducible), then p does not belong to any FactorSet α.

Русский

Если p не является неприводимым (то есть разлагаемым), то p не принадлежит ни одному FactorSet α.

LaTeX

$$hp : ¬Irreducible p → ∀ s : FactorSet α, p ∉ s$$

Lean4

theorem reducible_notMem_factorSet {p : Associates α} (hp : ¬Irreducible p) (s : FactorSet α) : p ∉ s := fun h ↦ by
  rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h

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