divisors_filter_dvd_of_dvd — Mathlib

English

If n ≠ 0 and m | n, then the filter of n.divisors by divisibility by m equals m.divisors.

Русский

Если n ≠ 0 и m|n, то фильтр делителей n по делимости на m равен делителям m.

LaTeX

$$$\\{d\\in n.divisors \\mid d|m\\} = m.divisors$ (при $n\\neq 0$ и $m\\mid n$)$$

Lean4

theorem divisors_filter_dvd_of_dvd {n m : ℕ} (hn : n ≠ 0) (hm : m ∣ n) : {d ∈ n.divisors | d ∣ m} = m.divisors :=
  by
  ext k
  simp_rw [mem_filter, mem_divisors]
  exact ⟨fun ⟨_, hkm⟩ ↦ ⟨hkm, ne_zero_of_dvd_ne_zero hn hm⟩, fun ⟨hk, _⟩ ↦ ⟨⟨hk.trans hm, hn⟩, hk⟩⟩

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