degree_prod_le — Mathlib

English

For a finite set s, deg_m(∏_{i∈s} P_i) ≤ ∑_{i∈s} deg_m(P_i).

Русский

Для конечного множества s выполняется deg_m(∏_{i∈s} P_i) ≤ ∑_{i∈s} deg_m(P_i).

LaTeX

$$$$ \deg_m\left( \prod_{i\in s} P_i \right) \preceq_m \sum_{i\in s} \deg_m(P_i). $$$$

Lean4

theorem degree_prod_le {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι} :
    m.degree (∏ i ∈ s, P i) ≼[m] ∑ i ∈ s, m.degree (P i) := by
  classical
    induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]

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