support_factorization — Mathlib

English

The support of factorization(n) equals the Finset of normalized factors of n.

Русский

Поддержка факторизации(n) совпадает с Finset нормализованных факторов n.

LaTeX

$$$\\text{support}(\\text{factorization}(n)) = (\\text{normalizedFactors}(n)).toFinset$$$

Lean4

/-- The support of `factorization n` is exactly the Finset of normalized factors -/
@[simp]
theorem support_factorization {n : α} : (factorization n).support = (normalizedFactors n).toFinset := by
  simp [factorization, Multiset.toFinsupp_support]

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