dvd_of_mem_divisors

Mathlib.NumberTheory.Divisors

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

English

If n ∈ divisors m, then n ∣ m.

Русский

Если n ∈ divisors(m), то n делит m.

LaTeX

$$$\forall \{n,m\} : \nexists,\ (n \in \mathrm{divisors}(m)) \Rightarrow n \mid m$$$

Lean4

theorem dvd_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ∣ m :=
  (mem_divisors.mp h).1

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

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

Разделы

Аффилиация

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