sub_toIcoDiv_zsmul_mem_Ico

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#sub_toIcoDiv_zsmul_mem_Ico

English

For b, a, p with p > 0, the integer n = toIcoDiv hp a b satisfies b − n·p ∈ [a, a+p).

Русский

Для b, a, p с p > 0 целое n = toIcoDiv hp a b удовлетворяет b − n·p ∈ [a, a+p).

LaTeX

$$$b - \mathrm{toIcoDiv}(hp,a,b) \cdot p \in [a, a+p)$$$

Lean4

theorem sub_toIcoDiv_zsmul_mem_Ico (a b : α) : b - toIcoDiv hp a b • p ∈ Set.Ico a (a + p) :=
  (existsUnique_sub_zsmul_mem_Ico hp b a).choose_spec.1

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

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

Разделы

Аффилиация

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