eval_unique — Mathlib

English

For any φ : R[X] →ₐ[R] A, φ(p) = eval₂(algebraMap R A, φ(X)) p for all p.

Русский

Для любого φ: R[X] →ₐ[R] A выполняется φ(p) = eval₂(∘, φ(X)) p для всех p.

LaTeX

$$$\forall \phi: R[X] \rightarrowₐ[R] A,\; \phi(p) = \operatorname{eval}_2(\operatorname{algebraMap} R A, \phi(X))\, p.$$$

Lean4

theorem eval_unique (φ : R[X] →ₐ[R] A) (p) : φ p = eval₂ (algebraMap R A) (φ X) p := by
  rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]

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