natDegree_multiset_prod — Mathlib

English

Let t be a multiset of polynomials with 0 ∉ t. Then natDegree t.prod = ∑ natDegree(p) for p in t.

Русский

Пусть t — мультимножество полиномов без нулевого элемента. Тогда natDegree произведения равно сумме natDegree каждого элемента.

LaTeX

$$$$\operatorname{natDegree}(t.prod) = \sum_{p\in t} \operatorname{natDegree}(p) \,\text{if } 0 \notin t.$$$$

Lean4

theorem natDegree_multiset_prod (h : (0 : R[X]) ∉ t) : natDegree t.prod = (t.map natDegree).sum :=
  by
  nontriviality R
  rw [natDegree_multiset_prod']
  simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]
  rintro ⟨_, h, rfl⟩
  contradiction

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