degree_prod — Mathlib

English

If each P_i ≠ 0 for i ∈ s, then deg_m(∏_{i∈s} P_i) = ∑_{i∈s} deg_m(P_i).

Русский

Если каждый P_i ≠ 0 для 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) = \sum_{i\in s} \deg_m(P_i). $$$$

Lean4

theorem degree_prod [IsCancelMulZero R] {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, P i ≠ 0) :
    m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i) :=
  by
  apply degree_prod_of_regular
  intro i hi
  apply isRegular_of_ne_zero
  rw [leadingCoeff_ne_zero_iff]
  exact H i hi

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