le_padicValNat_iff_replicate_subperm_primeFactorsList

English

For prime a and b ≠ 0, and any n, n ≤ padicValNat a b iff replicate n a is a sub-permutation of b’s primeFactorsList.

Русский

Для простого a и b ≠ 0, и любого n: n ≤ padicValNat a b тогда и только тогда, когда replicate n a является подпермуляцией primeFactorsList(b).

LaTeX

$$$\\\\forall a,b,n \\\\; (a \\\\text{ prime}) \\\\land (b \\\\neq 0) \\\\Rightarrow \\\\; n \\\\le \\\\mathrm{padicValNat}(a,b) \\\\Leftrightarrow (\\\\text{replicate } n\,a) \\\\lt+~\\\\, b.\\\\primeFactorsList$$$

Lean4

theorem le_padicValNat_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime) (hb : b ≠ 0) :
    n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList := by
  rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
    Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩ |>.emultiplicity_eq_multiplicity, ←
    padicValNat_def' ha.ne_one hb, Nat.cast_le]

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