map_div_left_divisors — Mathlib

English

There is a bijection between divisors(n) and divisorsAntidiagonal(n) given by d ↦ (n/d, d).

Русский

Существует биекция между делителями(n) и делителями антидиагонали по $d \mapsto (n/d, d)$.

LaTeX

$$$ \mathrm{divisorsAntidiagonal}(n) = \{(n/d, d) : d \in \mathrm{divisors}(n)\} \quad (\text{при } n>0) $$$

Lean4

theorem map_div_left_divisors :
    n.divisors.map ⟨fun d => (n / d, d), fun _ _ => congr_arg Prod.snd⟩ = n.divisorsAntidiagonal :=
  by
  apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
  ext
  rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
  simp

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