normalizedFactors_pos — Mathlib

English

For x ≠ 0, 0 < normalizedFactors x is equivalent to not IsUnit x.

Русский

Для x ≠ 0 верно, что 0 < normalizedFactors x тогда и только тогда, когда x не единица.

LaTeX

$$normalizedFactors_pos(x) ≡ 0 < normalizedFactors(x) ⇔ ¬IsUnit(x)$$

Lean4

@[simp]
theorem normalizedFactors_pos (x : α) (hx : x ≠ 0) : 0 < normalizedFactors x ↔ ¬IsUnit x :=
  by
  constructor
  · intro h hx
    obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
    exact (prime_of_normalized_factor _ hp).not_unit (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)
  · intro h
    obtain ⟨p, hp⟩ := exists_mem_normalizedFactors 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⟩))

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