le_infDegree_mul — Mathlib

English

For any AddZeroClass A and additive targets, f.infDegree(D) + g.infDegree(D) ≤ (f*g).infDegree(D) for D a suitable AddHom.

Русский

Для любых A и соответствующего отображения D верно неравенство о сумме инфDegree и инфDegree произведения.

LaTeX

$$$$f.infDegree_D + g.infDegree_D \le (f g).infDegree_D.$$$$

Lean4

theorem le_infDegree_mul [AddZeroClass A] [Add T] [AddLeftMono T] [AddRightMono T] (D : AddHom A T) (f g : R[A]) :
    f.infDegree D + g.infDegree D ≤ (f * g).infDegree D :=
  le_inf_support_mul (fun {a b : A} => (map_add D a b).ge) _ _

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