leadingCoeff_toLex_C

Mathlib.Algebra.MvPolynomial.Variables

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

English

The supremum degree with respect to toLex of the constant polynomial C r is 0 when r is the coefficient.

Русский

Предел максимальной степени по toLex для константного полинома C r равен 0.

LaTeX

$$$ \mathrm{supDegree}\ toLex\ (C\ (\sigma := \sigma)\ r) = 0 $$$

Lean4

theorem leadingCoeff_toLex_C (r : R) : leadingCoeff toLex (C (σ := σ) r) = r :=
  leadingCoeff_single toLex.injective _ r

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

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

Разделы

Аффилиация

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