degreeOf_X — Mathlib

English

The degree of X_j with respect to i is 1 if i = j and 0 otherwise (under appropriate nontriviality assumptions).

Русский

Степень X_j по i равна 1, если i = j, и 0 иначе (при соответствующих условиях не тривиальности).

LaTeX

$$$\deg_i(X_j) = \begin{cases} 1, & i = j \\ 0, & i \neq j \end{cases}$$$

Lean4

theorem degreeOf_X [DecidableEq σ] (i j : σ) [Nontrivial R] :
    degreeOf i (X j : MvPolynomial σ R) = if i = j then 1 else 0 := by
  classical
  by_cases c : i = j
  · simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, degreeOf_def, degrees_X]

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