fst_mem_divisors_of_mem_antidiagonal

Mathlib.NumberTheory.Divisors

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

← MathLib Explorer

English

If (x,y) ∈ divisorsAntidiagonal(n), then x ∈ divisors(n).

Русский

Если (x,y) ∈ divisorsAntidiagonal(n), тогда x ∈ divisors(n).

LaTeX

$$$ (x,y) \in n.divisorsAntidiagonal \Rightarrow x \in n.divisors$$$

Lean4

theorem fst_mem_divisors_of_mem_antidiagonal {x : ℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) : x.fst ∈ divisors n :=
  by
  rw [mem_divisorsAntidiagonal] at h
  simp [Dvd.intro _ h.1, h.2]

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

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

Разделы

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

Аффилиация

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