toIcoDiv_zsmul_sub_toIcoMod

Mathlib.Algebra.Order.ToIntervalMod

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

English

For all a, b ∈ α, b = (toIcoDiv(hp, a, b)) p + toIcoMod(hp, a, b).

Русский

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

LaTeX

$$$$\text{toIcoDiv}(hp, a, b) \cdot p + \text{toIcoMod}(hp, a, b) = b$$$$

Lean4

@[simp]
theorem toIcoDiv_zsmul_sub_toIcoMod (a b : α) : toIcoDiv hp a b • p + toIcoMod hp a b = b := by
  rw [add_comm, toIcoMod_add_toIcoDiv_zsmul]

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

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

Разделы

Аффилиация

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