toIocMod_add_right_eq_add — Mathlib

English

In the same setting with different index, the identity remains: toIcoMod hp a (b + c) = toIcoMod hp (a − c) b + c.

Русский

В той же настройке сохраняется тождество: toIcoMod hp a (b + c) = toIcoMod hp (a − c) b + c.

LaTeX

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

Lean4

theorem toIocMod_add_right_eq_add (a b c : α) : toIocMod hp a (b + c) = toIocMod hp (a - c) b + c := by
  simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]

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