primeFactors_of_isUnit — Mathlib

English

If an element is a unit, then it has no prime factors.

Русский

Если элемент является единицей (обратим), то у него нет простых делителей.

LaTeX

$$$ \operatorname{primeFactors}(a) = \emptyset \quad \text{если } IsUnit(a) $$$

Lean4

/-- If `x` is a unit, then the finset of prime factors of `x` is empty.
The converse is true with a nonzero assumption, see `primeFactors_eq_empty_iff`.
-/
theorem primeFactors_of_isUnit (h : IsUnit a) : primeFactors a = ∅ := by
  classical rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]

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