factors_eq_some_iff_ne_zero — Mathlib

English

An element a ≠ 0 has a representation a.factors as a finite multiset of irreducibles.

Русский

С ненулевого элемента a имеется представлениe a.factors в виде конечного мульти-множества неприводимых.

LaTeX

$$(∃ s : Multiset { p : Associates α // Irreducible p }, a.factors = s) ↔ a ≠ 0$$

Lean4

theorem factors_eq_some_iff_ne_zero {a : Associates α} :
    (∃ s : Multiset { p : Associates α // Irreducible p }, a.factors = s) ↔ a ≠ 0 :=
  by
  simp_rw [@eq_comm _ a.factors, ← WithTop.ne_top_iff_exists]
  exact factors_eq_top_iff_zero.not

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