English
For a natural number n, factorization(n) is the finitely supported function from primes to nonnegative integers that assigns to each prime p the p-adic valuation v_p(n) and assigns 0 to non-primes; its support is the set of prime divisors of n.
Русский
Для натурального числа n факторизация(n) — это конечно-поддерживаемая функция от простых чисел в неотрицательные целые числа, которая каждому простому p сопоставляет p-адическую кратность v_p(n), а не простым числам — 0; поддержка функции равна множеству простых делителей n.
LaTeX
$$Let n ∈ ℕ. The map factorization(n): ℕ →₀ ℕ is the finitely supported function with support = {p : p is prime and p ∣ n} and (factorization(n))(p) = { v_p(n) if p is prime, 0 otherwise }.$$
Lean4
/-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
mapping each prime factor of `n` to its multiplicity in `n`. -/
def factorization (n : ℕ) : ℕ →₀ ℕ where
support := n.primeFactors
toFun p := if p.Prime then padicValNat p n else 0
mem_support_toFun := by simp [not_or]; aesop
