# Lemmas about the `sup` and `inf` of the support of `AddMonoidAlgebra` #

## 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 `degree`s.

## sup-degree and inf-degree of an `AddMonoidAlgebra` #

Let `R` be a semiring and let `A` be a `SemilatticeSup`. For an element `f : R[A]`, this file defines

- `AddMonoidAlgebra.supDegree`: the sup-degree taking values in `WithBot A`,
- `AddMonoidAlgebra.infDegree`: the inf-degree taking values in `WithTop A`.

If the grading type `A` is a linearly ordered additive monoid, then these two notions of degree coincide with the standard one:

- the sup-degree is the maximum of the exponents of the monomials that appear with non-zero coefficient in `f`, or `⊥`, if `f = 0`;
- the inf-degree is the minimum of the exponents of the monomials that appear with non-zero coefficient in `f`, or `⊤`, if `f = 0`.

The main results are

- `AddMonoidAlgebra.supDegree_mul_le`: the sup-degree of a product is at most the sum of the sup-degrees,
- `AddMonoidAlgebra.le_infDegree_mul`: the inf-degree of a product is at least the sum of the inf-degrees,
- `AddMonoidAlgebra.supDegree_add_le`: the sup-degree of a sum is at most the sup of the sup-degrees,
- `AddMonoidAlgebra.le_infDegree_add`: the inf-degree of a sum is at least the inf of the inf-degrees.

### Implementation notes #

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 twice:

- once for `supDegree` (essentially a simple application) and
- once for `infDegree` (a simple application, via `OrderDual`).

These final lemmas are the ones that likely get used the most. The generic lemmas about `Finset.support.sup` may not be used directly much outside of this file. To see this in action, you can look at the triple `(sup_support_mul_le, maxDegree_mul_le, le_minDegree_mul)`.

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

source
theorem AddMonoidAlgebra.sup_support_add_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] (degb : A → B) (f g : AddMonoidAlgebra R A) :
(f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb
source
theorem AddMonoidAlgebra.le_inf_support_add {R : Type u_1} {A : Type u_3} {T : Type u_4} [SemilatticeInf T] [OrderTop T] [Semiring R] (degt : A → T) (f g : AddMonoidAlgebra R A) :
f.support.inf degt ⊓ g.support.inf degt ≤ (f + g).support.inf degt
source
theorem AddMonoidAlgebra.sup_support_mul_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [Add A] [Add B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (f g : AddMonoidAlgebra R A) :
(f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
source
theorem AddMonoidAlgebra.le_inf_support_mul {R : Type u_1} {A : Type u_3} {T : Type u_4} [SemilatticeInf T] [OrderTop T] [Semiring R] [Add A] [Add T] [AddLeftMono T] [AddRightMono T] {degt : A → T} (degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)) (f g : AddMonoidAlgebra R A) :
f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt
source
theorem AddMonoidAlgebra.sup_support_list_prod_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [AddMonoid A] [AddMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (l : List (AddMonoidAlgebra R A)) :
l.prod.support.sup degb ≤ (List.map (fun (f : AddMonoidAlgebra R A) => f.support.sup degb) l).sum
source
theorem AddMonoidAlgebra.le_inf_support_list_prod {R : Type u_1} {A : Type u_3} {T : Type u_4} [SemilatticeInf T] [OrderTop T] [Semiring R] [AddMonoid A] [AddMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T} (degt0 : 0 ≤ degt 0) (degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)) (l : List (AddMonoidAlgebra R A)) :
(List.map (fun (f : AddMonoidAlgebra R A) => f.support.inf degt) l).sum ≤ l.prod.support.inf degt
source
theorem AddMonoidAlgebra.sup_support_pow_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [Semiring R] [AddMonoid A] [AddMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (n : ℕ) (f : AddMonoidAlgebra R A) :
(f ^ n).support.sup degb ≤ n • f.support.sup degb
source
theorem AddMonoidAlgebra.le_inf_support_pow {R : Type u_1} {A : Type u_3} {T : Type u_4} [SemilatticeInf T] [OrderTop T] [Semiring R] [AddMonoid A] [AddMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T} (degt0 : 0 ≤ degt 0) (degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)) (n : ℕ) (f : AddMonoidAlgebra R A) :
n • f.support.inf degt ≤ (f ^ n).support.inf degt
source
theorem AddMonoidAlgebra.sup_support_multiset_prod_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (m : Multiset (AddMonoidAlgebra R A)) :
m.prod.support.sup degb ≤ (Multiset.map (fun (f : AddMonoidAlgebra R A) => f.support.sup degb) m).sum
source
theorem AddMonoidAlgebra.le_inf_support_multiset_prod {R : Type u_1} {A : Type u_3} {T : Type u_4} [SemilatticeInf T] [OrderTop T] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T} (degt0 : 0 ≤ degt 0) (degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)) (m : Multiset (AddMonoidAlgebra R A)) :
(Multiset.map (fun (f : AddMonoidAlgebra R A) => f.support.inf degt) m).sum ≤ m.prod.support.inf degt
source
theorem AddMonoidAlgebra.sup_support_finset_prod_le {R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [SemilatticeSup B] [OrderBot B] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B} (degb0 : degb 0 ≤ 0) (degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b) (s : Finset ι) (f : ι → AddMonoidAlgebra R A) :
(∏ i ∈ s, f i).support.sup degb ≤ ∑ i ∈ s, (f i).support.sup degb
source
theorem AddMonoidAlgebra.le_inf_support_finset_prod {R : Type u_1} {A : Type u_3} {T : Type u_4} {ι : Type u_6} [SemilatticeInf T] [OrderTop T] [CommSemiring R] [AddCommMonoid A] [AddCommMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T} (degt0 : 0 ≤ degt 0) (degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)) (s : Finset ι) (f : ι → AddMonoidAlgebra R A) :
∑ i ∈ s, (f i).support.inf degt ≤ (∏ i ∈ s, f i).support.inf degt

### Shorthands for special cases #

Note that these definitions are reducible, in order to make it easier to apply the more generic lemmas above.

source
@[reducible, inline]
abbrev AddMonoidAlgebra.supDegree {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] (D : A → B) (f : AddMonoidAlgebra R A) :
B

Let `R` be a semiring, let `A` be an `AddZeroClass`, let `B` be an `OrderBot`, and let `D : A → B` be a "degree" function. For an element `f : R[A]`, the element `supDegree f : B` is the supremum of all the elements in the support of `f`, or `⊥` if `f` is zero. Often, the Type `B` is `WithBot A`, If, further, `A` has a linear order, then this notion coincides with the usual one, using the maximum of the exponents.

If `A := σ →₀ ℕ` then `R[A] = MvPolynomial σ R`, and if we equip `σ` with a linear order then the induced linear order on `Lex A` equips `MvPolynomial` ring with a monomial order (i.e. a linear order on `A`, the type of (monic) monomials in `R[A]`, that respects addition). We make use of this monomial order by taking `D := toLex`, and different monomial orders could be accessed via different type synonyms once they are added.

Equations

- AddMonoidAlgebra.supDegree D f = f.support.sup D

Instances For

source
theorem AddMonoidAlgebra.supDegree_add_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {f g : AddMonoidAlgebra R A} :
supDegree D (f + g) ≤ supDegree D f ⊔ supDegree D g
source
@[simp]
theorem AddMonoidAlgebra.supDegree_neg {R' : Type u_2} {A : Type u_3} {B : Type u_5} [Ring R'] [SemilatticeSup B] [OrderBot B] {D : A → B} {f : AddMonoidAlgebra R' A} :
supDegree D (-f) = supDegree D f
source
theorem AddMonoidAlgebra.supDegree_sub_le {R' : Type u_2} {A : Type u_3} {B : Type u_5} [Ring R'] [SemilatticeSup B] [OrderBot B] {D : A → B} {f g : AddMonoidAlgebra R' A} :
supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g
source
theorem AddMonoidAlgebra.supDegree_sum_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} :
supDegree D (∑ i ∈ s, f i) ≤ s.sup fun (i : ι) => supDegree D (f i)
source
theorem AddMonoidAlgebra.supDegree_single_ne_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} (a : A) {r : R} (hr : r ≠ 0) :
supDegree D (single a r) = D a
source
theorem AddMonoidAlgebra.supDegree_single {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} (a : A) (r : R) :
supDegree D (single a r) = if r = 0 then ⊥ else D a
source
theorem AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {p : AddMonoidAlgebra R A} {a : A} (hlt : ¬D a ≤ supDegree D p) :
p a = 0
source
theorem AddMonoidAlgebra.supDegree_withBot_some_comp {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
supDegree (WithBot.some ∘ D) s = ↑(supDegree D s)
source
theorem AddMonoidAlgebra.supDegree_eq_of_isMaxOn {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {p : AddMonoidAlgebra R A} {a : A} (hmem : a ∈ p.support) (hmax : IsMaxOn D (↑p.support) a) :
supDegree D p = D a
source
@[simp]
theorem AddMonoidAlgebra.supDegree_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} [AddZeroClass A] :
supDegree D 0 = ⊥
source
theorem AddMonoidAlgebra.ne_zero_of_supDegree_ne_bot {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} [AddZeroClass A] {p : AddMonoidAlgebra R A} :
supDegree D p ≠ ⊥ → p ≠ 0
source
theorem AddMonoidAlgebra.ne_zero_of_not_supDegree_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} [AddZeroClass A] {p : AddMonoidAlgebra R A} {b : B} (h : ¬supDegree D p ≤ b) :
p ≠ 0
source
theorem AddMonoidAlgebra.supDegree_eq_of_max {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} [AddZeroClass A] {p : AddMonoidAlgebra R A} {b : B} (hb : b ∈ Set.range D) (hmem : Function.invFun D b ∈ p.support) (hmax : ∀ a ∈ p.support, D a ≤ b) :
supDegree D p = b
source
theorem AddMonoidAlgebra.supDegree_mul_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} [AddZeroClass A] {p q : AddMonoidAlgebra R A} [Add B] (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [AddLeftMono B] [AddRightMono B] :
supDegree D (p * q) ≤ supDegree D p + supDegree D q
source
theorem AddMonoidAlgebra.supDegree_prod_le {R : Type u_7} {A : Type u_8} {B : Type u_9} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [SemilatticeSup B] [OrderBot B] [AddLeftMono B] [AddRightMono B] {D : A → B} (hzero : D 0 = 0) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) {ι : Type u_10} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} :
supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
source
theorem AddMonoidAlgebra.apply_add_of_supDegree_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} [AddZeroClass A] {p q : AddMonoidAlgebra R A} [Add B] (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) {ap aq : A} (hp : supDegree D p ≤ D ap) (hq : supDegree D q ≤ D aq) :
(p * q) (ap + aq) = p ap * q aq
source
noncomputable def AddMonoidAlgebra.leadingCoeff {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] (D : A → B) [Nonempty A] (f : AddMonoidAlgebra R A) :
R

If `D` is an injection into a linear order `B`, the leading coefficient of `f : R[A]` is the nonzero coefficient of highest degree according to `D`, or 0 if `f = 0`. In general, it is defined to be the coefficient at an inverse image of `supDegree f` (if such exists).

Equations

- AddMonoidAlgebra.leadingCoeff D f = f (Function.invFun D (AddMonoidAlgebra.supDegree D f))

Instances For

source
@[reducible]
def AddMonoidAlgebra.Monic {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] (D : A → B) [Nonempty A] (f : AddMonoidAlgebra R A) :
Prop

An element `f : R[A]` is monic if its leading coefficient is one.

Equations

- AddMonoidAlgebra.Monic D f = (AddMonoidAlgebra.leadingCoeff D f = 1)

Instances For

source
@[simp]
theorem AddMonoidAlgebra.leadingCoeff_single {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} [Nonempty A] (hD : Function.Injective D) (a : A) (r : R) :
leadingCoeff D (single a r) = r
source
@[simp]
theorem AddMonoidAlgebra.leadingCoeff_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} [Nonempty A] :
leadingCoeff D 0 = 0
source
theorem AddMonoidAlgebra.Monic.ne_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p : AddMonoidAlgebra R A} {D : A → B} [Nonempty A] [Nontrivial R] (hp : Monic D p) :
p ≠ 0
source
@[simp]
theorem AddMonoidAlgebra.monic_one {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} [AddZeroClass A] (hD : Function.Injective D) :
Monic D 1
source
theorem AddMonoidAlgebra.exists_supDegree_mem_support {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p : AddMonoidAlgebra R A} (D : A → B) (hp : p ≠ 0) :
∃ a ∈ p.support, supDegree D p = D a
source
theorem AddMonoidAlgebra.supDegree_mem_range {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p : AddMonoidAlgebra R A} (D : A → B) (hp : p ≠ 0) :
supDegree D p ∈ Set.range D
source
theorem AddMonoidAlgebra.supDegree_sum_lt {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} (hs : s.Nonempty) {b : B} (h : ∀ i ∈ s, supDegree D (f i) < b) :
supDegree D (∑ i ∈ s, f i) < b
source
theorem AddMonoidAlgebra.supDegree_add_eq_left {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (h : supDegree D q < supDegree D p) :
supDegree D (p + q) = supDegree D p
source
theorem AddMonoidAlgebra.supDegree_add_eq_right {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (h : supDegree D p < supDegree D q) :
supDegree D (p + q) = supDegree D q
source
theorem AddMonoidAlgebra.leadingCoeff_add_eq_left {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (h : supDegree D q < supDegree D p) :
leadingCoeff D (p + q) = leadingCoeff D p
source
theorem AddMonoidAlgebra.leadingCoeff_add_eq_right {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (h : supDegree D p < supDegree D q) :
leadingCoeff D (p + q) = leadingCoeff D q
source
theorem AddMonoidAlgebra.supDegree_mem_support {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (hD : Function.Injective D) (hp : p ≠ 0) :
Function.invFun D (supDegree D p) ∈ p.support
source
@[simp]
theorem AddMonoidAlgebra.leadingCoeff_eq_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (hD : Function.Injective D) :
leadingCoeff D p = 0 ↔ p = 0
source
theorem AddMonoidAlgebra.leadingCoeff_ne_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] (hD : Function.Injective D) :
leadingCoeff D p ≠ 0 ↔ p ≠ 0
source
theorem AddMonoidAlgebra.supDegree_sub_lt_of_leadingCoeff_eq {A : Type u_3} {B : Type u_5} [LinearOrder B] [OrderBot B] {D : A → B} [AddZeroClass A] (hD : Function.Injective D) {R : Type u_8} [Ring R] {p q : AddMonoidAlgebra R A} (hd : supDegree D p = supDegree D q) (hc : leadingCoeff D p = leadingCoeff D q) :
supDegree D (p - q) < supDegree D p ∨ p = q
source
theorem AddMonoidAlgebra.supDegree_leadingCoeff_sum_eq {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} {ι : Type u_7} {s : Finset ι} {i : ι} {f : ι → AddMonoidAlgebra R A} [AddZeroClass A] (hi : i ∈ s) (hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)) :
supDegree D (∑ j ∈ s, f j) = supDegree D (f i) ∧ leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)
source
theorem AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree' {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} [AddZeroClass A] (hs : ∃ i ∈ s, f i ≠ 0) (hd : Set.InjOn (supDegree D ∘ f) ↑s) :
∑ i ∈ s, f i ≠ 0
source
theorem AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} [AddZeroClass A] (hs : s ≠ ∅) (hf : ∀ i ∈ s, f i ≠ 0) (hd : Set.InjOn (supDegree D ∘ f) ↑s) :
∑ i ∈ s, f i ≠ 0
source
theorem AddMonoidAlgebra.apply_supDegree_add_supDegree {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) :
(p * q) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
source
theorem AddMonoidAlgebra.supDegree_mul {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hpq : leadingCoeff D p * leadingCoeff D q ≠ 0) (hp : p ≠ 0) (hq : q ≠ 0) :
supDegree D (p * q) = supDegree D p + supDegree D q
source
theorem AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hq : Monic D q) (hp : p ≠ 0) :
supDegree D (p * q) = supDegree D p + supDegree D q
source
theorem AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : Monic D p) (hq : q ≠ 0) :
supDegree D (p * q) = supDegree D p + supDegree D q
source
theorem AddMonoidAlgebra.Monic.supDegree_mul {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hbot : ⊥ + ⊥ = ⊥) (hp : Monic D p) (hq : Monic D q) :
supDegree D (p * q) = supDegree D p + supDegree D q
source
theorem AddMonoidAlgebra.leadingCoeff_mul {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] [NoZeroDivisors R] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) :
leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
source
theorem AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hq : Monic D q) :
leadingCoeff D (p * q) = leadingCoeff D p
source
theorem AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : Monic D p) :
leadingCoeff D (p * q) = leadingCoeff D q
source
theorem AddMonoidAlgebra.Monic.mul {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : Monic D p) (hq : Monic D q) :
Monic D (p * q)
source
theorem AddMonoidAlgebra.Monic.pow {R : Type u_1} [Semiring R] {A : Type u_8} {B : Type u_9} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B} {p : AddMonoidAlgebra R A} {n : ℕ} (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hD : Function.Injective D) (hp : Monic D p) :
Monic D (p ^ n)
source
theorem AddMonoidAlgebra.Monic.supDegree_pow {R : Type u_1} [Semiring R] {A : Type u_8} {B : Type u_9} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B} {p : AddMonoidAlgebra R A} {n : ℕ} (hzero : D 0 = 0) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hD : Function.Injective D) [Nontrivial R] (hp : Monic D p) :
supDegree D (p ^ n) = n • supDegree D p
source
@[reducible, inline]
abbrev AddMonoidAlgebra.infDegree {R : Type u_1} {A : Type u_3} {T : Type u_4} [Semiring R] [SemilatticeInf T] [OrderTop T] (D : A → T) (f : AddMonoidAlgebra R A) :
T

Let `R` be a semiring, let `A` be an `AddZeroClass`, let `T` be an `OrderTop`, and let `D : A → T` be a "degree" function. For an element `f : R[A]`, the element `infDegree f : T` is the infimum of all the elements in the support of `f`, or `⊤` if `f` is zero. Often, the Type `T` is `WithTop A`, If, further, `A` has a linear order, then this notion coincides with the usual one, using the minimum of the exponents.

Equations

- AddMonoidAlgebra.infDegree D f = f.support.inf D

Instances For

source
theorem AddMonoidAlgebra.le_infDegree_add {R : Type u_1} {A : Type u_3} {T : Type u_4} [Semiring R] [SemilatticeInf T] [OrderTop T] (D : A → T) (f g : AddMonoidAlgebra R A) :
infDegree D f ⊓ infDegree D g ≤ infDegree D (f + g)
source
theorem AddMonoidAlgebra.infDegree_withTop_some_comp {R : Type u_1} {A : Type u_3} {T : Type u_4} [Semiring R] [SemilatticeInf T] [OrderTop T] {D : A → T} {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
infDegree (WithTop.some ∘ D) s = ↑(infDegree D s)
source
theorem AddMonoidAlgebra.le_infDegree_mul {R : Type u_1} {A : Type u_3} {T : Type u_4} [Semiring R] [SemilatticeInf T] [OrderTop T] [AddZeroClass A] [Add T] [AddLeftMono T] [AddRightMono T] (D : A →ₙ+ T) (f g : AddMonoidAlgebra R A) :
infDegree (⇑D) f + infDegree (⇑D) g ≤ infDegree (⇑D) (f * g)