algebraMap_eq

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.algebraMap_eq

English

The algebra map from R to R[X] coincides with the canonical C map: algebraMap R R[X] = C.

Русский

АлгебраMap из R в R[X] совпадает с канонической картой C: algebraMap R R[X] = C.

LaTeX

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

Lean4

@[simp]
theorem algebraMap_eq : algebraMap R R[X] = C :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru