C

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.C

English

The canonical algebra map from R into MvPolynomial σ R coincides with the embedding C.

Русский

Каноническое отображение алгебра из R в MvPolynomial σ R совпадает с вложением C.

LaTeX

$$$ \text{algebraMap}_R(\MvPolynomial(σ,R)) = C $$$

Lean4

/-- `C a` is the constant polynomial with value `a` -/
def C : R →+* MvPolynomial σ R :=
  { singleZeroRingHom with toFun := monomial 0 }

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

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

Разделы

Аффилиация

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