monomial_mul_X

Mathlib.Algebra.Polynomial.Basic

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

English

Multiplying a monomial by X shifts the exponent by one: monomial n r · X = monomial(n + 1) r.

Русский

Умножение монома на X увеличивает показатель степени на единицу: monomial n r · X = monomial(n + 1) r.

LaTeX

$$monomial(n, r) * X = monomial(n + 1, r)$$

Lean4

@[simp]
theorem monomial_mul_X (n : ℕ) (r : R) : monomial n r * X = monomial (n + 1) r := by
  rw [X, monomial_mul_monomial, mul_one]

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

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

Разделы

Аффилиация

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