image_snd_divisorsAntidiagonal — Mathlib

English

The second-coordinate image of divisorsAntidiagonal(n) equals divisors(n).

Русский

Вторая координата изображений делителей антидиагонали образует делители числа n.

LaTeX

$$$ (divisorsAntidiagonal(n)).image Prod.snd = divisors(n) $$$

Lean4

@[simp]
theorem image_snd_divisorsAntidiagonal : (divisorsAntidiagonal n).image Prod.snd = divisors n :=
  by
  rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
  exact image_fst_divisorsAntidiagonal

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