English
The product of the first and second components of divisorsAntidiagonalFactors equals the original n, proving the factorization property along the antidiagonal.
Русский
Произведение первых компонент divisorsAntidiagonalFactors равно исходному n, доказывая разложение по антидиагонали.
LaTeX
$$$$ (divisorsAntidiagonalFactors n x).1.1 \cdot (divisorsAntidiagonalFactors n x).2.1 = n. $$$$
Lean4
/-- The map from `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b`
to `(a, b)`. -/
def divisorsAntidiagonalFactors (n : ℕ+) : Nat.divisorsAntidiagonal n → ℕ+ × ℕ+ := fun x ↦
⟨⟨x.1.1, Nat.pos_of_mem_divisors (Nat.fst_mem_divisors_of_mem_antidiagonal x.2)⟩,
(⟨x.1.2, Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal x.2)⟩ : ℕ+),
Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal x.2)⟩
