toIcoMod_sub' — Mathlib

English

For all a,b ∈ α and m ∈ Z, we have toIcoMod hp (a − m·p) b = toIcoMod hp a b − m·p.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toIcoMod_sub' (a b : α) : toIcoMod hp (a - p) b = toIcoMod hp a b - p := by
  simpa only [one_zsmul] using toIcoMod_sub_zsmul' hp a b 1

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