English
For prime a and hb ≠ 0, replicate n a is a subpermutation of b.primeFactorsList if and only if a^n divides b.
Русский
Для простого a и hb ≠ 0, список повторений a по длине n является подперму primeFactorsList(b) тогда и только тогда, когда a^n делит b.
LaTeX
$$Prime(a) → Ne(b,0) → replicate(n,a) <+~ b.primeFactorsList iff a^n ∣ b$$
Lean4
theorem replicate_subperm_primeFactorsList_iff {a b n : ℕ} (ha : Prime a) (hb : b ≠ 0) :
replicate n a <+~ primeFactorsList b ↔ a ^ n ∣ b := by
induction n generalizing b with
| zero => simp
| succ n ih =>
constructor
· rw [List.subperm_iff]
rintro ⟨u, hu1, hu2⟩
rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
exact hu2.prod_dvd_prod
· rintro ⟨c, rfl⟩
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
rw [pow_succ', mul_assoc, replicate_succ, (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left,
primeFactorsList_prime ha, singleton_append, subperm_cons, ih hb.2]
exact dvd_mul_right _ _
