negSucc_zsmul — Mathlib

English

For every a in G and every natural number n, the action of −(n+1) on a equals the additive inverse of (n+1) times a: (−(n+1)) • a = −((n+1) • a).

Русский

Для любого элемента a в G и любого натурального числа n выполняется (- (n+1)) • a = −((n+1) • a).

LaTeX

$$$(- (n+1)) \\cdot a = -\\big((n+1) \\cdot a\\big)$$$

Lean4

theorem negSucc_zsmul {G} [SubNegMonoid G] (a : G) (n : ℕ) : Int.negSucc n • a = -((n + 1) • a) :=
  by
  rw [← natCast_zsmul]
  exact SubNegMonoid.zsmul_neg' n a

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