degree_X — Mathlib

English

The degree of X_s equals the unit vector at s with weight 1.

Русский

Степень X_s равна единичному вектору, сосредоточенному в координате s, со значением 1.

LaTeX

$$$m.degree(X_s) = \\ Finsupp.single s 1$$$

Lean4

theorem degree_X [Nontrivial R] {s : σ} : m.degree (X s : MvPolynomial σ R) = Finsupp.single s 1 := by
  classical
  change m.degree (monomial (Finsupp.single s 1) (1 : R)) = _
  rw [degree_monomial, if_neg one_ne_zero]

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