algebraMap_comp_C — Mathlib

English

Let K be a commutative domain. The canonical map from polynomials K[X] to RatFunc K, when composed with the embedding of constants Polynomial.C, equals the canonical constant embedding C: K → RatFunc K.

Русский

Пусть K — коммутативное домножение. Каноническое отображение из полиномов K[X] в RatFunc K, сопоставляющее константам константы, совпадает с каноничным вложением C: K → RatFunc K.

LaTeX

$$$ (\mathrm{algebraMap}_{K[X] \to \mathrm{RatFunc} K}) \circ \mathrm{Polynomial.C} = \mathrm{C} $$$

Lean4

@[simp]
theorem algebraMap_comp_C : (algebraMap K[X] (RatFunc K)).comp Polynomial.C = C :=
  rfl

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