English
For prime a and b ≠ 0, and any n, we have ↑n ≤ emultiplicity a b iff the list replicate n a is a sub-permutation of b’s primeFactorsList.
Русский
Для простого a и b ≠ 0 выполняется: ↑n ≤ emultiplicity a b эквивалентно тому, что список replicate n a является под-частью списка простых факторов b.
LaTeX
$$$\\\\uparrow n \\\\le \\\\operatorname{emultiplicity} a b \\\\Longleftrightarrow (\\\\text{replicate } n\,a) \\,<+~\\\\, b.\\\\primeFactorsList$$$
Lean4
theorem le_emultiplicity_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime) (hb : b ≠ 0) :
↑n ≤ emultiplicity a b ↔ replicate n a <+~ b.primeFactorsList :=
(replicate_subperm_primeFactorsList_iff ha hb).trans pow_dvd_iff_le_emultiplicity |>.symm