Lemmas on infinite sums over the antidiagonal of the divisors function

This file contains lemmas about the antidiagonal of the divisors function. It defines the map from Nat.divisorsAntidiagonal n to ℕ+ × ℕ+ given by sending n = a * b to (a, b).

def divisorsAntidiagonalFactors (n : ℕ+) : { x : ℕ × ℕ // x ∈ (↑n).divisorsAntidiagonal } → ℕ+ × ℕ+

The map from Nat.divisorsAntidiagonal n to ℕ+ × ℕ+ given by sending n = a * b to (a , b).

Equations

• divisorsAntidiagonalFactors n x = (⟨(↑x).1, ⋯⟩, ⟨↑⟨(↑x).2, ⋯⟩, ⋯⟩)

theorem divisorsAntidiagonalFactors_eq {n : ℕ+} (x : { x : ℕ × ℕ // x ∈ (↑n).divisorsAntidiagonal }) : ↑(divisorsAntidiagonalFactors n x).1 * ↑(divisorsAntidiagonalFactors n x).2 = ↑n

theorem divisorsAntidiagonalFactors_one (x : { x : ℕ × ℕ // x ∈ Nat.divisorsAntidiagonal 1 }) : divisorsAntidiagonalFactors 1 x = (1, 1)

def sigmaAntidiagonalEquivProd : (n : ℕ+) × { x : ℕ × ℕ // x ∈ (↑n).divisorsAntidiagonal } ≃ ℕ+ × ℕ+

The equivalence from the union over n of Nat.divisorsAntidiagonal n to ℕ+ × ℕ+ given by sending n = a * b to (a , b).

Equations

• One or more equations did not get rendered due to their size.

theorem sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) : ↑(sigmaAntidiagonalEquivProd.symm x).fst = ↑x.1 * ↑x.2

theorem sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) : ↑(sigmaAntidiagonalEquivProd.symm x).snd = (↑x.1, ↑x.2)