English
For any n and k with k ≠ 0, n.primeFactorsList is a sublist of (n·k).primeFactorsList.
Русский
Для любых n и k с k ≠ 0, n.primeFactorsList является подподсписком (n·k).primeFactorsList.
LaTeX
$$k ≠ 0 → n.primeFactorsList <+ (n*k).primeFactorsList$$
Lean4
theorem primeFactorsList_sublist_right {n k : ℕ} (h : k ≠ 0) : n.primeFactorsList <+ (n * k).primeFactorsList :=
by
rcases n with - | hn
· simp [zero_mul]
apply sublist_of_subperm_of_sorted _ (primeFactorsList_sorted _) (primeFactorsList_sorted _)
simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]
exact (sublist_append_left _ _).subperm