primeFactors_eq_empty_iff — Mathlib

English

For a ≠ 0, the finite set of prime factors of a is empty if and only if a is a unit.

Русский

Для a ≠ 0 множество простых делителей a пусто тогда и только тогда, когда a является единицей.

LaTeX

$$$ a \neq 0 \Rightarrow \big( \operatorname{primeFactors}(a) = \emptyset \iff IsUnit(a) \big) $$$

Lean4

/-- The finset of prime factors of `x` is empty if and only if `x` is a unit.
The converse is true without the nonzero assumption, see `primeFactors_of_isUnit`.
-/
theorem primeFactors_eq_empty_iff (ha : a ≠ 0) : primeFactors a = ∅ ↔ IsUnit a := by
  classical rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff ha]

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