primeFactorsList_sublist_right — Mathlib

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

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