English
There is a natural bijection between the disjoint union over n of the antidiagonal n and the product A×A, given by mapping (n,(k,l)) to (k,l) with inverse (k,l) ↦ (k+l,(k,l)).
Русский
Существует естественная биекция между дизъюнктным объединением по всем n антидиагоналям n и произведением A×A, задаваемая переходом (n,(k,l)) ↦ (k,l) с обратным переходом (k,l) ↦ (k+l,(k,l)).
LaTeX
$$$ (\\Sigma n : A,\\; antidiagonal(n)) \\cong A \\times A, \\quad (n,(k,l)) \\mapsto (k,l), \\quad (k,l) \\mapsto (k+l,(k,l)). $$$
Lean4
/-- The disjoint union of antidiagonals `Σ (n : A), antidiagonal n` is equivalent to the product
`A × A`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`. -/
@[simps]
def sigmaAntidiagonalEquivProd [AddMonoid A] [HasAntidiagonal A] : (Σ n : A, antidiagonal n) ≃ A × A
where
toFun x := x.2
invFun x := ⟨x.1 + x.2, x, mem_antidiagonal.mpr rfl⟩
left_inv := by
rintro ⟨n, ⟨k, l⟩, h⟩
rw [mem_antidiagonal] at h
exact Sigma.subtype_ext h rfl
