toIcoMod_add_right_eq_add — Mathlib

English

For all a,b,c ∈ α, the equality holds: toIcoMod hp a (b + c) = toIcoMod hp (a − c) b + c.

Русский

Для любых a,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 toIcoMod_add_right_eq_add (a b c : α) : toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c := by
  simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]

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