le_of_dvd

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.le_of_dvd

English

If m ∣ n then m ≤ n.

Русский

Если m делит n, то m ≤ n.

LaTeX

$$$$ m \mid n \Rightarrow m \le n $$$$

Lean4

theorem le_of_dvd {m n : ℕ+} : m ∣ n → m ≤ n := by
  rw [dvd_iff']
  intro h
  rw [← h]
  apply (mod_le n m).left

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

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

Разделы

Аффилиация

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