one_def

Mathlib.Algebra.MvPolynomial.Basic

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

English

The multiplicative identity in MvPolynomial is the monomial with exponent 0 and coefficient 1: 1 = monomial 0 1.

Русский

Единичный элемент в MvPolynomial равен мономиалу с нулевым показателем и коэффициентом 1: 1 = monomial 0 1.

LaTeX

$$$ (1 : MvPolynomial \; σ\; R) = monomial 0 1 $$$

Lean4

theorem one_def : (1 : MvPolynomial σ R) = monomial 0 1 :=
  rfl

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

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

Разделы

Аффилиация

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