factorization — Mathlib

English

The factorization maps an element to its irreducible factor multiplicities, represented as a finitely supported function. It is defined by taking the multiset of irreducible factors and converting it to a finsupp.

Русский

Факторизация отображает элемент в множество кратностей простых факторов в виде конечной опоры.

LaTeX

$$$\\text{factorization}(n) = \\operatorname{Multiset}.toFinsupp(\\operatorname{normalizedFactors}(n))$$$

Lean4

/-- This returns the multiset of irreducible factors as a `Finsupp`. -/
noncomputable def factorization (n : α) : α →₀ ℕ :=
  Multiset.toFinsupp (normalizedFactors n)

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