dvd_of_mod_eq_zero — Mathlib

English

Let a and b be ordinals. If a mod b = 0, then b divides a; equivalently, there exists q with a = b · q.

Русский

Пусть a и b — ординалы. Если a mod b = 0, то b делит a; эквивалентно существует q такие, что a = b · q.

LaTeX

$$$a \bmod b = 0 \Rightarrow \exists q, a = b \cdot q$$$

Lean4

theorem dvd_of_mod_eq_zero {a b : Ordinal} (H : a % b = 0) : b ∣ a :=
  ⟨a / b, by simpa [H] using (div_add_mod a b).symm⟩

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