totalDegree_add_eq_right_of_totalDegree_lt

English

Degree of i in a finite sum is bounded by the supremum over indices of degreeOf i (f_j).

Русский

Степень i в конечной сумме ограничена сверху степеней по индексам f_j.

LaTeX

$$$\deg_i\left(\sum_{j} f_j\right) \le \sup_j \deg_i(f_j)$$$

Lean4

theorem totalDegree_add_eq_right_of_totalDegree_lt {p q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) :
    (q + p).totalDegree = p.totalDegree := by rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]

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