primeFactors_filter_dvd_of_dvd — Mathlib

English

If n ≠ 0 and m | n, then the set { p ∈ n.primeFactors | p | m } equals m.primeFactors.

Русский

Если n ≠ 0 и m делит n, то множество { p ∈ n.primeFactors | p | m } равно m.primeFactors.

LaTeX

$$$\{ p \in n.primeFactors \mid p \mid m \} = m.primeFactors,$ with the conditions $n \neq 0$ and $m \mid n$.$$

Lean4

theorem primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) :
    {p ∈ n.primeFactors | p ∣ m} = m.primeFactors := by
  simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm, divisors_filter_dvd_of_dvd hn hmn]

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