primeFactorsList_sublist_of_dvd — Mathlib

English

If n ∣ k and k ≠ 0, then n.primeFactorsList is a sublist of k.primeFactorsList.

Русский

Если n делится на k и k ≠ 0, то n.primeFactorsList является подподсписком k.primeFactorsList.

LaTeX

$$n ∣ k ∧ k ≠ 0 → n.primeFactorsList <+ k.primeFactorsList$$

Lean4

theorem primeFactorsList_sublist_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : n.primeFactorsList <+ k.primeFactorsList :=
  by
  obtain ⟨a, rfl⟩ := h
  exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

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