image_piFinTwoEquiv_finMulAntidiag

English

For n, the image of finMulAntidiag 2 n under piFinTwoEquiv equals the divisorsAntidiagonal of n.

Русский

Для n образ finMulAntidiag 2 n под piFinTwoEquiv равен divisorsAntidiagonal n.

LaTeX

$$$(\text{finMulAntidiag}\ 2\ n).image\ (\piFinTwoEquiv\ (\lambda x,\mathbb{N})) = \text{divisorsAntidiagonal}(n)$$$

Lean4

theorem image_piFinTwoEquiv_finMulAntidiag {n : ℕ} :
    (finMulAntidiag 2 n).image (piFinTwoEquiv <| fun _ => ℕ) = divisorsAntidiagonal n :=
  by
  ext x
  simp [(piFinTwoEquiv <| fun _ => ℕ).symm.surjective.exists]

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