English
For a finite index set s and a family f_i ∈ R[A], the supremum degree of the product ∏_{i∈s} f_i is at most the sum of the supremum degrees of the factors.
Русский
Пусть s конечен; для семейства f_i ∈ R[A], тогда supDegree D(∏_{i∈s} f_i) ≤ ∑_{i∈s} supDegree D(f_i).
LaTeX
$$$\left(\prod_{i \in s} f_i\right).supDegree D \le \sum_{i \in s} (f_i).supDegree D$$$
Lean4
theorem supDegree_prod_le {R A B : Type*} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [SemilatticeSup B]
[OrderBot B] [AddLeftMono B] [AddRightMono B] {D : A → B} (hzero : D 0 = 0)
(hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) {ι} {s : Finset ι} {f : ι → R[A]} :
(∏ i ∈ s, f i).supDegree D ≤ ∑ i ∈ s, (f i).supDegree D := by
classical
refine s.induction ?_ ?_
· rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
split_ifs; exacts [bot_le, hzero.le]
· intro i s his ih
rw [Finset.prod_insert his, Finset.sum_insert his]
exact (supDegree_mul_le hadd).trans (by gcongr)
