toIcoMod_sub — Mathlib

English

For all a,b ∈ α and p > 0, the subtraction by p in the right argument reduces to: toIcoMod hp a (b − p) = toIcoMod hp a b.

Русский

Для любых a,b ∈ α и p > 0 высказывается: toIcoMod hp a (b − p) = toIcoMod hp a b.

LaTeX

$$$\forall a,b \in \alpha,\; toIcoMod\ hp\ a\ (b - p) = toIcoMod\ hp\ a\ b$$$

Lean4

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

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