divisorsAntidiagonalFactors_one — Mathlib

English

In the n=1 case, divisorsAntidiagonalFactors returns (1,1) for the canonical representation.

Русский

В случае n=1 divisorsAntidiagonalFactors возвращает (1,1) для канонического представления.

LaTeX

$$$$ divisorsAntidiagonalFactors(1, x) = (1,1). $$$$

Lean4

theorem divisorsAntidiagonalFactors_one (x : Nat.divisorsAntidiagonal 1) : (divisorsAntidiagonalFactors 1 x) = (1, 1) :=
  by
  have h := Nat.mem_divisorsAntidiagonal.mp x.2
  simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h
  simp [divisorsAntidiagonalFactors, h.1, h.2]

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