aeval_unique — Mathlib

English

A polynomial-algebra hom φ is determined by φ ∘ X, i.e., φ = aeval (φ ∘ X). This expresses the uniqueness of the evaluation map.

Русский

Гомоморфизм алгебр φ определяется по φ ∘ X, то есть φ = aeval (φ ∘ X).

LaTeX

$$$\\\\forall \\phi: MvPolynomial σ R \\to[R] S_1, \\phi = \\\\mathrm{aeval} (\\\\phi \\\\circ X)$$$

Lean4

theorem aeval_unique (φ : MvPolynomial σ R →ₐ[R] S₁) : φ = aeval (φ ∘ X) :=
  by
  ext i
  simp

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