CAlgHom

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

The constant polynomial map C defines an R-algebra hom from A to A[X].

Русский

Постоянный полином C задает R-алгебра-гомоморфизм из A в A[X].

LaTeX

$$$\mathrm{CAlgHom}: A \to_R A[X]$$$

Lean4

/-- `Polynomial.C` as an `AlgHom`. -/
@[simps! apply]
def CAlgHom : A →ₐ[R] A[X] where
  toRingHom := C
  commutes' _ := rfl

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

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

Разделы

Аффилиация

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