factors_pos — Mathlib

English

If x ≠ 0, then 0 < factors(x) is equivalent to x not being a unit.

Русский

Если x ≠ 0, то количество факторов положительно тогда и только тогда, когда x не единица.

LaTeX

$$$x \neq 0 \Rightarrow 0 < \mathrm{factors}(x) \;\iff\; \neg \mathrm{IsUnit}(x).$$$

Lean4

@[simp]
theorem factors_pos (x : α) (hx : x ≠ 0) : 0 < factors x ↔ ¬IsUnit x :=
  by
  constructor
  · intro h hx
    obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
    exact (prime_of_factor _ hp).not_unit (isUnit_of_dvd_unit (dvd_of_mem_factors hp) hx)
  · intro h
    obtain ⟨p, hp⟩ := exists_mem_factors hx h
    exact bot_lt_iff_ne_bot.mpr (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

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