map_prodComm_divisorsAntidiag — Mathlib

English

The divisors antidiagonal of z is invariant under swapping the two coordinates, i.e., mapping by the coordinate-swap permutation leaves z.divisorsAntidiag unchanged.

Русский

Антидиагональ делителей z сохраняется при обмене координат — отображение по перестановке координат не меняет множество z.divisorsAntidiag.

LaTeX

$$$ \text{map}_{\text{swap}}(z.divisorsAntidiag) = z.divisorsAntidiag $$$

Lean4

@[simp]
theorem map_prodComm_divisorsAntidiag : z.divisorsAntidiag.map (Equiv.prodComm _ _).toEmbedding = z.divisorsAntidiag :=
  by ext; simp [mem_divisorsAntidiag]

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