map_prodComm_antidiagonal — Mathlib

English

Applying the product-commutativity equivalence to the antidiagonal preserves the set; the mapped set under prodComm equals the original antidiagonal.

Русский

Применение эквивалентности перестановки координат к антидиагонали сохраняет множество; отображение через prodComm даёт ту же антидиагональ.

LaTeX

$$$\\operatorname{map}(\\mathrm{Equiv.prodComm}\\, A A)\\bigl(\\operatorname{antidiagonal}(n)\\bigr) = \\operatorname{antidiagonal}(n)$$$

Lean4

@[simp]
theorem map_prodComm_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
    (antidiagonal n).map (Equiv.prodComm A A) = antidiagonal n :=
  Finset.ext fun ⟨a, b⟩ => by simp [add_comm]

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