toIcoMod_add_left — Mathlib

English

In the standard setting, adding p to the second argument inside IcoMod leaves the value unchanged: toIcoMod hp a (p + b) = toIcoMod hp a b.

Русский

В обычной конфигурации прибавление p к второму аргументу внутри IcoMod не меняет значение: toIcoMod hp a (p + b) = toIcoMod hp a b.

LaTeX

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

Lean4

@[simp]
theorem toIcoMod_add_left (a b : α) : toIcoMod hp a (p + b) = toIcoMod hp a b := by rw [add_comm, toIcoMod_add_right]

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