English
Same flavor as the previous lemma: the infDegree of a product dominates the sum of infDegrees.
Русский
То же самое: infDegree произведения доминирует над суммой infDegree.
LaTeX
$$$$f.infDegree_D + g.infDegree_D \le (f g).infDegree_D.$$$$
Lean4
/-- Divide by `of' k G g`, discarding terms not divisible by this. -/
noncomputable def divOf [IsCancelAdd G] (x : k[G]) (g : G) : k[G] :=
-- note: comapping by `+ g` has the effect of subtracting `g` from every element in
-- the support, and discarding the elements of the support from which `g` can't be subtracted.
-- If `G` is an additive group, such as `ℤ` when used for `LaurentPolynomial`,
-- then no discarding occurs.
@Finsupp.comapDomain.addMonoidHom _ _ _ _ (g + ·) (add_right_injective g) x
