ofFinsupp_algebraMap — Mathlib

English

For any r ∈ R, the element ⟨algebraMap R _ r⟩ viewed as a polynomial equals algebraMap R A[X] r.

Русский

Для любого r ∈ R элемент ⟨algebraMap R _ r⟩, рассматриваемый как многочлен, равен algebraMap R A[X] r.

LaTeX

$$$ (\langle \mathrm{algebraMap}\; R\; \_\; r \rangle: A[X]) = \mathrm{algebraMap}\; R\; A[X]\; r $$$

Lean4

theorem ofFinsupp_algebraMap (r : R) : (⟨algebraMap R _ r⟩ : A[X]) = algebraMap R A[X] r :=
  toFinsupp_injective (toFinsupp_algebraMap _).symm

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