toIocDiv_zsmul_sub_toIocMod

Mathlib.Algebra.Order.ToIntervalMod

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

English

For all a, b ∈ α, b = (toIocDiv(hp, a, b)) p + toIocMod(hp, a, b).

Русский

Для любых a, b ∈ α выполняется разложение b = (toIocDiv(hp, a, b)) p + toIocMod(hp, a, b).

LaTeX

$$$$\text{toIocDiv}(hp, a, b) \cdot p + \text{toIocMod}(hp, a, b) = b$$$$

Lean4

@[simp]
theorem toIocDiv_zsmul_sub_toIocMod (a b : α) : toIocDiv hp a b • p + toIocMod hp a b = b := by
  rw [add_comm, toIocMod_add_toIocDiv_zsmul]

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

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

Разделы

Аффилиация

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