dvd_iff_mod_eq_zero

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For ordinals a,b, b divides a if and only if a mod b = 0.

Русский

Для ординалов a и b верно: b делит a тогда же, когда a mod b = 0.

LaTeX

$$$b \mid a \iff a \bmod b = 0$$$

Lean4

theorem dvd_iff_mod_eq_zero {a b : Ordinal} : b ∣ a ↔ a % b = 0 :=
  ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩

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

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

Разделы

Аффилиация

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