toIcoMod_sub_zsmul' — Mathlib

English

In an Archimedean ordered additive group, for all a, b ∈ α and m ∈ Z, the right-hand side satisfies 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_zsmul' (a b : α) (m : ℤ) : toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p := by
  simp_rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_zsmul']

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