map_aeval — Mathlib

English

If adjoin(R s) = ⊤ and two derivations agree on s, then they are equal.

Русский

Если adjoin(R s) = ⊤ и две производные совпадают на s, то они равны.

LaTeX

$$adjoin\,R\,s = \top \ ∧ \ Set.EqOn D1 D2 s \Rightarrow D1 = D2$$

Lean4

@[simp]
theorem map_aeval (P : R[X]) (x : A) : D (aeval x P) = aeval x (derivative P) • D x :=
  by
  induction P using Polynomial.induction_on
  · simp
  · simp [add_smul, *]
  · simp [mul_smul, ← Nat.cast_smul_eq_nsmul A]

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