map_swap_divisorsAntidiagonal — Mathlib

English

The divisors antidiagonal is invariant under swapping the two coordinates.

Русский

Антидиагональ делителей инвариантна к обмену координат.

LaTeX

$$$ (divisorsAntidiagonal(n)).map (Equiv.prodComm _ _).toEmbedding = divisorsAntidiagonal(n) $$$

Lean4

@[simp]
theorem map_swap_divisorsAntidiagonal :
    (divisorsAntidiagonal n).map (Equiv.prodComm _ _).toEmbedding = divisorsAntidiagonal n :=
  by
  rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm, Set.image_swap_eq_preimage_swap]
  ext
  exact swap_mem_divisorsAntidiagonal

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