divisorsAntidiagonalFactors_eq — Mathlib

English

For any x in the 1-based divisorsAntidiagonal, the product of the coordinates recovers n.

Русский

Для любого x в 1-базовой divisorsAntidiagonal произведение координат восстанавливает n.

LaTeX

$$$$ (divisorsAntidiagonalFactors n x).fst.val \cdot (divisorsAntidiagonalFactors n x).snd.val = n. $$$$

Lean4

theorem divisorsAntidiagonalFactors_eq {n : ℕ+} (x : Nat.divisorsAntidiagonal n) :
    (divisorsAntidiagonalFactors n x).1.1 * (divisorsAntidiagonalFactors n x).2.1 = n := by
  simp [divisorsAntidiagonalFactors, (Nat.mem_divisorsAntidiagonal.mp x.2).1]

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