smeval_neg_nat — Mathlib

English

For a nonassociative ring S and a natural polynomial q, evaluating at −n (in S) equals evaluating at −n (as an integer) in S: q.smeval (−n : S) = q.smeval (−n : ℤ).

Русский

Для неассоциированного кольца S и q ∈ ℕ[X], значение в −n в S равно значению в −n как целого числа: q.smeval (−n : S) = q.smeval (−n : ℤ).

LaTeX

$$$$ q.smeval (-(n : S)) = q.smeval (-n : \mathbb{Z}). $$$$

Lean4

theorem smeval_neg_nat (S : Type*) [NonAssocRing S] [Pow S ℕ] [NatPowAssoc S] (q : ℕ[X]) (n : ℕ) :
    q.smeval (-(n : S)) = q.smeval (-n : ℤ) :=
  by
  rw [smeval_eq_sum, smeval_eq_sum]
  simp only [Polynomial.smul_pow, sum_def]
  simp

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