C_eq_algebraMap — Mathlib

English

For a commutative semiring R, the polynomial constant map C is equal to the base algebra map algebraMap R R[X].

Русский

Для коммутативного полускольного кольца R отображение константного полинома C совпадает с базовым алгебраическим отображением algebraMap R R[X].

LaTeX

$$$ C = \mathrm{algebraMap}\; R \; R[X] $$$

Lean4

/-- When we have `[CommSemiring R]`, the function `C` is the same as `algebraMap R R[X]`.

(But note that `C` is defined when `R` is not necessarily commutative, in which case
`algebraMap` is not available.)
-/
theorem C_eq_algebraMap (r : R) : C r = algebraMap R R[X] r :=
  rfl

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