map_swap_antidiagonal — Mathlib

English

If you map the antidiagonal by swapping the two components of each pair, you obtain the same antidiagonal.

Русский

Если сопряжение пары в антидиагонали поменять местами, то антидиагональ не изменится.

LaTeX

$$$\\operatorname{(antidiagonal}(n)).\\mathrm{map}(\\mathrm{Prod.swap}) = \\operatorname{antidiagonal}(n).$$$

Lean4

theorem map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map Prod.swap = antidiagonal n := by
  rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]

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