toIocMod_sub_zsmul' — Mathlib

English

For a in α, b in α and m in Z, we have toIocMod hp (a − m·p) b = toIocMod hp a b − m·p.

Русский

Для любых a, b ∈ α и m ∈ Z выполняется toIocMod hp (a − m·p) b = toIocMod hp a b − m·p.

LaTeX

$$$\forall a,b \in \alpha\,\forall m \in \mathbb{Z},\; toIocMod\ hp\ (a - m\cdot p)\ b = toIocMod\ hp\ a\ b - m\cdot p$$$

Lean4

@[simp]
theorem toIocMod_sub_zsmul' (a b : α) (m : ℤ) : toIocMod hp (a - m • p) b = toIocMod hp a b - m • p := by
  simp_rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul']

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