image_div_divisors_eq_divisors — Mathlib

English

For a natural number n, the image of the map x ↦ n/x on the divisors of n equals the divisors of n.

Русский

Для натурального n образ отображения x ↦ n/x на делителях n равен делителям n.

LaTeX

$$$\mathrm{image}\bigl(\lambda x:\mathbb{N}.\, n/x\bigr)(n.divisors) = n.divisors.$$$

Lean4

@[simp]
theorem image_div_divisors_eq_divisors (n : ℕ) : image (fun x : ℕ => n / x) n.divisors = n.divisors :=
  by
  by_cases hn : n = 0
  · simp [hn]
  ext a
  constructor
  · rw [mem_image]
    rintro ⟨x, hx1, hx2⟩
    rw [mem_divisors] at *
    refine ⟨?_, hn⟩
    rw [← hx2]
    exact div_dvd_of_dvd hx1.1
  · rw [mem_divisors, mem_image]
    rintro ⟨h1, -⟩
    exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩

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