le_inf_support_multiset_prod — Mathlib

English

The sup degree bound for a multiset of elements in an additive monoid algebra holds, mirroring the finite multiset/prod bound via quotients.

Русский

Предел верхней грани поддержки множества элементов в аддитивной алгебре моноидов сохраняется аналогично конечному списку через эквивалентные представления.

LaTeX

$$$\\text{For } m:\\text{Multiset}(R[A]),\\; (m.Trans)\\;\\sup deg ≤ (m.map f).sum$$$

Lean4

theorem le_inf_support_multiset_prod (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))
    (m : Multiset R[A]) : (m.map fun f : R[A] => f.support.inf degt).sum ≤ m.prod.support.inf degt :=
  by
  refine
    OrderDual.ofDual_le_ofDual.mpr <|
      sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_) (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
  · exact degt0
  · exact degtm _ _

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