# mathlib3documentation

algebra.monoid_algebra.degree

# Lemmas about the sup and inf of the support of add_monoid_algebra#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## TODO #

The current plan is to state and prove lemmas about finset.sup (finsupp.support f) D with a "generic" degree/weight function D from the grading Type A to a somewhat ordered Type B.

Next, the general lemmas get specialized for some yet-to-be-defined degrees.

### Results about the finset.sup and finset.inf of finsupp.support#

In this section, we use degb and degt to denote "degree functions" on A with values in a type with bot or top respectively.

theorem add_monoid_algebra.sup_support_add_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [order_bot B] [semiring R] (degb : A B) (f g : A) :
(f + g).support.sup degb f.support.sup degb g.support.sup degb
theorem add_monoid_algebra.le_inf_support_add {R : Type u_1} {A : Type u_2} {T : Type u_3} [order_top T] [semiring R] (degt : A T) (f g : A) :
f.support.inf degt g.support.inf degt (f + g).support.inf degt
theorem add_monoid_algebra.sup_support_mul_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [order_bot B] [semiring R] [has_add A] [has_add B] {degb : A B} (degbm : {a b : A}, degb (a + b) degb a + degb b) (f g : A) :
(f * g).support.sup degb f.support.sup degb + g.support.sup degb
theorem add_monoid_algebra.le_inf_support_mul {R : Type u_1} {A : Type u_2} {T : Type u_3} [order_top T] [semiring R] [has_add A] [has_add T] {degt : A T} (degtm : {a b : A}, degt a + degt b degt (a + b)) (f g : A) :
f.support.inf degt + g.support.inf degt (f * g).support.inf degt
theorem add_monoid_algebra.sup_support_list_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [order_bot B] [semiring R] [add_monoid A] [add_monoid B] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (l : list A)) :
l.prod.support.sup degb (list.map (λ (f : , f.support.sup degb) l).sum
theorem add_monoid_algebra.le_inf_support_list_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} [order_top T] [semiring R] [add_monoid A] [add_monoid T] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (l : list A)) :
(list.map (λ (f : , f.support.inf degt) l).sum l.prod.support.inf degt
theorem add_monoid_algebra.sup_support_pow_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [order_bot B] [semiring R] [add_monoid A] [add_monoid B] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (n : ) (f : A) :
(f ^ n).support.sup degb n f.support.sup degb
theorem add_monoid_algebra.le_inf_support_pow {R : Type u_1} {A : Type u_2} {T : Type u_3} [order_top T] [semiring R] [add_monoid A] [add_monoid T] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (n : ) (f : A) :
n f.support.inf degt (f ^ n).support.inf degt
theorem add_monoid_algebra.sup_support_multiset_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [order_bot B] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (m : multiset A)) :
m.prod.support.sup degb (multiset.map (λ (f : , f.support.sup degb) m).sum
theorem add_monoid_algebra.le_inf_support_multiset_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} [order_top T] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (m : multiset A)) :
(multiset.map (λ (f : , f.support.inf degt) m).sum m.prod.support.inf degt
theorem add_monoid_algebra.sup_support_finset_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} {ι : Type u_5} [order_bot B] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (s : finset ι) (f : ι ) :
(s.prod (λ (i : ι), f i)).support.sup degb s.sum (λ (i : ι), (f i).support.sup degb)
theorem add_monoid_algebra.le_inf_support_finset_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} {ι : Type u_5} [order_top T] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (s : finset ι) (f : ι ) :
s.sum (λ (i : ι), (f i).support.inf degt) (s.prod (λ (i : ι), f i)).support.inf degt