smeval_at_natCast — Mathlib

English

For q ∈ ℕ[X], and n ∈ ℕ, q.smeval (n : S) = q.smeval n, i.e., behavior under natural casts commutes with smeval.

Русский

Для q ∈ ℕ[X] и n ∈ ℕ, q.smeval (n : S) = q.smeval n; поведение при приведение к S согласуется с smeval.

LaTeX

$$$$ \forall q : \mathbb{N}[X], \forall n : \mathbb{N}, q.smeval (n : S) = q.smeval n. $$$$

Lean4

theorem smeval_at_natCast (q : ℕ[X]) : ∀ (n : ℕ), q.smeval (n : S) = q.smeval n := by
  induction q using Polynomial.induction_on' with
  | add p q ph qh =>
    intro n
    simp only [smeval_add, ph, qh, Nat.cast_add]
  | monomial n a =>
    intro n
    rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]

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