vars_monomial_single — Mathlib

English

For a monomial with a single variable index i, exponent e>0 and nonzero coefficient r, the variables are exactly {i}.

Русский

Для монома с единственным индексом i, степенью e>0 и ненулевым коэффициентом r переменные равны {i}.

LaTeX

$$$ (\mathrm{monomial}(\mathrm{Finsupp}.single\ i\ e)\ r).vars = \{i\} $$$

Lean4

theorem vars_monomial_single (i : σ) {e : ℕ} {r : R} (he : e ≠ 0) (hr : r ≠ 0) :
    (monomial (Finsupp.single i e) r).vars = { i } := by rw [vars_monomial hr, Finsupp.support_single_ne_zero _ he]

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