divisor_le

Mathlib.NumberTheory.Divisors

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

← MathLib Explorer

English

If n ∈ divisors m, then n ≤ m.

Русский

Если n принадлежит divisors m, то n ≤ m.

LaTeX

$$$n \\in \\mathrm{divisors}(m) \\Rightarrow n \\le m$$$

Lean4

theorem divisor_le {m : ℕ} : n ∈ divisors m → n ≤ m :=
  by
  rcases m with - | m
  · simp
  · simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]
    exact Nat.le_of_dvd (Nat.succ_pos m)

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

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

Разделы

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

Аффилиация

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