mod_lt

Mathlib.Algebra.EuclideanDomain.Defs

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.mod_lt

English

For any a and nonzero b in a Euclidean domain, a mod b is strictly less than b with respect to the Euclidean order.

Русский

Для любых a и не нуля b в евклидовом кольце остаток a mod b строго меньше b по евклидову порядку.

LaTeX

$$$$ b \\neq 0 \\Rightarrow a \\% b \\prec b. $$$$

Lean4

theorem mod_lt : ∀ (a) {b : R}, b ≠ 0 → a % b ≺ b :=
  EuclideanDomain.remainder_lt

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

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

Разделы

Аффилиация

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