degreeOf_prod_le — Mathlib

English

Degree of i in p^n is at most n times degreeOf i p.

Русский

Степень i в p^n не больше n умноженного на deg_i p.

LaTeX

$$$\deg_i(p^n) \le n \cdot \deg_i p$$$

Lean4

theorem degreeOf_prod_le {ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
    degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, (f j).degreeOf i :=
  by
  simp_rw [degreeOf_eq_sup]
  exact
    supDegree_prod_le (by simp only [coe_zero, Pi.zero_apply])
      (by simp)
        -- TODO we can prove equality with `NoZeroDivisors R`

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