degreeOf_zero — Mathlib

English

Degree of i in f · g is bounded by the sum of degrees of i in f and i in g: degreeOf i (f g) ≤ degreeOf i f + degreeOf i g.

Русский

Степень i в произведении f g не превышает суммы степеней i в f и i в g.

LaTeX

$$$\deg_i(fg) \le \deg_i(f) + \deg_i(g)$$$

Lean4

@[simp]
theorem degreeOf_zero (n : σ) : degreeOf n (0 : MvPolynomial σ R) = 0 := by
  classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]

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