monomial_one_one_eq_X

Mathlib.Algebra.Polynomial.Basic

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

English

The monomial of degree 1 with coefficient 1 equals X: monomial(1,1) = X.

Русский

Мономиал степени 1 с коэффициентом 1 равен X: monomial(1,1) = X.

LaTeX

$$$ \operatorname{monomial}(1,1) = X $$$

Lean4

theorem monomial_one_one_eq_X : monomial 1 (1 : R) = X :=
  rfl

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

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

Разделы

Аффилиация

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