S_neg_sub_one — Mathlib

English

Let R be a commutative ring and n an integer. Then S_R(-n-1) = -S_R(n-1).

Русский

Пусть R — коммутативное кольцо, n — целое число. Тогда S_R(-n-1) = -S_R(n-1).

LaTeX

$$$\forall n \in \mathbb{Z},\ S_R(-n-1) = -S_R(n-1).$$$

Lean4

theorem S_neg_sub_one (n : ℤ) : S R (-n - 1) = -S R (n - 1) := by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := S_add_one R n
    have h₂ := S_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_eq R n
    have h₂ := S_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂

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