image_fst_divisorsAntidiagonal

Mathlib.NumberTheory.Divisors

URI: https://scilib.ai/kg/mathlib#Nat.image_fst_divisorsAntidiagonal

← MathLib Explorer

English

The first-coordinate image of divisorsAntidiagonal(n) equals divisors(n).

Русский

Первая координата изображений делителей антидиагонали образует делители числа n.

LaTeX

$$$ (divisorsAntidiagonal(n)).image Prod.fst = divisors(n) $$$

Lean4

@[simp]
theorem image_fst_divisorsAntidiagonal : (divisorsAntidiagonal n).image Prod.fst = divisors n :=
  by
  ext
  simp [Dvd.dvd, @eq_comm _ n (_ * _)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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