factors_one — Mathlib

English

The multiset of prime factors of the unit 1 is empty.

Русский

Мультсет простых факторов единицы равен пустому набору.

LaTeX

$$$\mathrm{factors}(1) = 0$$$

Lean4

@[simp]
theorem factors_one : factors (1 : α) = 0 := by
  nontriviality α using factors
  rw [← Multiset.rel_zero_right]
  refine factors_unique irreducible_of_factor (fun x hx => (Multiset.notMem_zero x hx).elim) ?_
  rw [Multiset.prod_zero]
  exact factors_prod one_ne_zero

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