degree_prod_of_regular — Mathlib

English

If for all i in s, IsRegular(leadingCoeff(P_i)), then deg_m(∏_{i∈s} P_i) = ∑_{i∈s} deg_m(P_i).

Русский

Если для всех i в s выполняется IsRegular(leadingCoeff(P_i)), то 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_of_regular {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι}
    (H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) : m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i) := by
  cases subsingleton_or_nontrivial R with
  | inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
  | inr _ =>
    apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    rw [mem_support_iff, m.coeff_prod_sum_degree]
    exact (IsRegular.prod H).ne_zero

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