smeval_natCast — Mathlib

English

For any natural n, the smeval of n viewed as a polynomial (n : R[X]) equals n times x^0: (n : R[X]).smeval x = n • x^0.

Русский

Для натурального n, smeval числа n как полинома равен n • x^0: (n : R[X]).smeval x = n • x^0.

LaTeX

$$$$ \forall n \in \mathbb{N},\ (n : R[X]).smeval x = n \cdot x^0. $$$$

Lean4

theorem smeval_natCast (n : ℕ) : (n : R[X]).smeval x = n • x ^ 0 := by
  induction n with
  | zero => simp only [smeval_zero, Nat.cast_zero, zero_smul]
  | succ n ih => rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]

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