normalizedFactors_eq_zero_iff — Mathlib

English

For x, the normalized factors are zero exactly when x is a unit (under a nonzero assumption).

Русский

Нормализованные факторы равны нулю тогда и только тогда, когда x является единицей (при условии ненулевости).

LaTeX

$$normalizedFactors_eq_zero_iff {x} (hx : x ≠ 0) : normalizedFactors x = 0 ↔ IsUnit x$$

Lean4

/-- The multiset of normalized factors of `x` is nil if and only if `x` is a unit.
The converse is true without the nonzero assumption, see `normalizedFactors_of_isUnit`.
-/
theorem normalizedFactors_eq_zero_iff {x : α} (hx : x ≠ 0) : normalizedFactors x = 0 ↔ IsUnit x := by
  rw [← not_iff_not, ← normalizedFactors_pos _ hx, pos_iff_ne_zero]

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