toIcoMod_zsmul_add — Mathlib

English

Shifting the inner second argument by m p leaves the IcoMod invariant: toIcoMod hp a (m p + b) = toIcoMod hp a b.

Русский

Сдвиг внутреннего второго аргумента на m p не изменяет IcoMod: toIcoMod hp a (m p + b) = toIcoMod hp a b.

LaTeX

$$$\operatorname{toIcoMod}\\_{hp} a (m \cdot p + b) = \operatorname{toIcoMod}\\_{hp} a b$$$

Lean4

@[simp]
theorem toIcoMod_zsmul_add (a b : α) (m : ℤ) : toIcoMod hp a (m • p + b) = toIcoMod hp a b := by
  rw [add_comm, toIcoMod_add_zsmul]

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