def negEquiv : ℤ ≃ ℤ

Equations

• negEquiv = { toFun := fun (n : ℤ) => -n, invFun := fun (n : ℤ) => -n, left_inv := negEquiv._proof_1, right_inv := negEquiv._proof_1 }

def succEquiv : ℤ ≃ ℤ

Equations

• succEquiv = { toFun := fun (n : ℤ) => n.succ, invFun := fun (n : ℤ) => n.pred, left_inv := Int.pred_succ, right_inv := Int.succ_pred }

def swap {α : Type u_1} : (Fin 2 → α) → Fin 2 → α

Equations

• swap x = ![x 1, x 0]

@[simp]

theorem swap_apply {α : Type u_1} (b : Fin 2 → α) : swap b = ![b 1, b 0]

theorem swap_involutive {α : Type u_1} (b : Fin 2 → α) : swap (swap b) = b

def swap_equiv {α : Type u_1} : (Fin 2 → α) ≃ (Fin 2 → α)

Equations

• swap_equiv = { toFun := swap, invFun := swap, left_inv := ⋯, right_inv := ⋯ }

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

Equations

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

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

Equations

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