divisorsAntidiagonal_one

Mathlib.NumberTheory.Divisors

URI: https://scilib.ai/kg/mathlib#Int.divisorsAntidiagonal_one

English

The divisorsAntidiag of 1 consists of exactly (1,1) and (-1,-1).

Русский

DivisorsAntidiag от 1 состоит ровно из (1,1) и (-1,-1).

LaTeX

$$$\operatorname{divisorsAntidiag}(1) = \{(1,1), (-1,-1)\}.$$$

Lean4

@[simp]
theorem divisorsAntidiagonal_one : Int.divisorsAntidiag 1 = {(1, 1), (-1, -1)} :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru