le_of_dvd

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

If b ≠ 0 and a divides b, then a ≤ b.

Русский

Если b ≠ 0 и a делит b, то a ≤ b.

LaTeX

$$∀ {a b : \\operatorname{Ordinal}}, b ≠ 0 → a ∣ b → a ≤ b$$

Lean4

theorem le_of_dvd : ∀ {a b : Ordinal}, b ≠ 0 → a ∣ b → a ≤ b
  | a, _, b0, ⟨b, e⟩ => by
    subst e
    simpa only [mul_one] using mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => by simp [h] at b0) a

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

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

Разделы

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

Аффилиация

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