leadingCoeff_prod_of_regular — Mathlib

English

If for all i, IsRegular(leadingCoeff(P_i)) for the finite set s, then lc_m(∏_{i∈s} P_i) = ∏_{i∈s} lc_m(P_i).

Русский

Если для всех i из конечного множества s выполняется регулярность lc_m(P_i), то lc_m(∏_{i∈s} P_i) = ∏ lc_m(P_i).

LaTeX

$$$$ \operatorname{leadingCoeff}_m\left( \prod_{i\in s} P_i \right) = \prod_{i\in s} \operatorname{leadingCoeff}_m(P_i). $$$$

Lean4

theorem leadingCoeff_prod_of_regular {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι}
    (H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) : m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i) :=
  by simp only [leadingCoeff, degree_prod_of_regular H, coeff_prod_sum_degree]

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