English
For all n,k with k ≠ 0, n.primeFactorsList.Sublist (n·k).primeFactorsList.
Русский
Для всех n,k с k ≠ 0, n.primeFactorsList является подподсписком (n·k).primeFactorsList.
LaTeX
$$k ≠ 0 → n.primeFactorsList.Sublist (n*k).primeFactorsList$$
Lean4
theorem dvd_of_primeFactorsList_subperm {a b : ℕ} (ha : a ≠ 0) (h : a.primeFactorsList <+~ b.primeFactorsList) :
a ∣ b := by
rcases b.eq_zero_or_pos with (rfl | hb)
· exact dvd_zero _
rcases a with (_ | _ | a)
· exact (ha rfl).elim
· exact one_dvd _
use (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
nth_rw 1 [← Nat.prod_primeFactorsList ha]
rw [← List.prod_append, List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
Nat.prod_primeFactorsList hb.ne']
