monomialOneHom_apply

Mathlib.Algebra.MvPolynomial.Basic

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

English

The value of the monomialOneHom on s is exactly the polynomial monomial(s,1).

Русский

Значение monomialOneHom на s равно мономулярному(s,1).

LaTeX

$$$\mathrm{monomialOneHom}\,R\,\sigma\,s = \mathrm{monomial}(s,1)$$$

Lean4

@[simp]
theorem monomialOneHom_apply : monomialOneHom R σ s = (monomial s 1 : MvPolynomial σ R) :=
  rfl

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

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

Разделы

Аффилиация

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