monomial_add_single — Mathlib

English

Adding a single exponent to a monomial corresponds to multiplying by X_n^e.

Русский

Прибавление к мономиалу единичной компоненты даёт произведение на X_n^e.

LaTeX

$$$\mathrm{monomial}(s + \mathcal{Finsupp.single(n,e)}, a) = \mathrm{monomial}(s,a) \cdot X_n^e$$$

Lean4

theorem monomial_add_single : monomial (s + Finsupp.single n e) a = monomial s a * X n ^ e := by
  rw [X_pow_eq_monomial, monomial_mul, mul_one]

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