map_swap_antidiagonal — Mathlib

English

There is a canonical equality between the antidiagonal mapped by swap and the original antidiagonal.

Русский

Существует каноническое равенство между антидиагональю после применения перестановки и исходной антидиагональю.

LaTeX

$$$(\\operatorname{antidiagonal}(n)).\\mathrm{map}(\\langle \\mathrm{Prod.swap}, \\mathrm{Prod.swap_injective}\\rangle) = \\operatorname{antidiagonal}(n)$$$

Lean4

/-- See also `Finset.map_prodComm_antidiagonal`. -/
@[simp]
theorem map_swap_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
    (antidiagonal n).map ⟨Prod.swap, Prod.swap_injective⟩ = antidiagonal n :=
  map_prodComm_antidiagonal

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