# Division of AddMonoidAlgebra by monomials #

This file is most important for when G = ℕ (polynomials) or G = σ →₀ ℕ (multivariate polynomials).

In order to apply in maximal generality (such as for LaurentPolynomials), this uses ∃ d, g' = g + d in many places instead of g ≤ g'.

## Main definitions #

• AddMonoidAlgebra.divOf x g: divides x by the monomial AddMonoidAlgebra.of k G g
• AddMonoidAlgebra.modOf x g: the remainder upon dividing x by the monomial AddMonoidAlgebra.of k G g.

## Main results #

• AddMonoidAlgebra.divOf_add_modOf, AddMonoidAlgebra.modOf_add_divOf: divOf and modOf are well-behaved as quotient and remainder operators.

## Implementation notes #

∃ d, g' = g + d is used as opposed to some other permutation up to commutativity in order to match the definition of semigroupDvd. The results in this file could be duplicated for MonoidAlgebra by using g ∣ g', but this can't be done automatically, and in any case is not likely to be very useful.

noncomputable def AddMonoidAlgebra.divOf {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) :

Divide by of' k G g, discarding terms not divisible by this.

Equations
• x.divOf g =
Instances For
@[simp]
theorem AddMonoidAlgebra.divOf_apply {k : Type u_1} {G : Type u_2} [] (g : G) (x : ) (g' : G) :
(x.divOf g) g' = x (g + g')
@[simp]
theorem AddMonoidAlgebra.support_divOf {k : Type u_1} {G : Type u_2} [] (g : G) (x : ) :
(x.divOf g).support = x.support.preimage (fun (x : G) => g + x)
@[simp]
theorem AddMonoidAlgebra.zero_divOf {k : Type u_1} {G : Type u_2} [] (g : G) :
@[simp]
theorem AddMonoidAlgebra.divOf_zero {k : Type u_1} {G : Type u_2} [] (x : ) :
x.divOf 0 = x
theorem AddMonoidAlgebra.add_divOf {k : Type u_1} {G : Type u_2} [] (x : ) (y : ) (g : G) :
(x + y).divOf g = x.divOf g + y.divOf g
theorem AddMonoidAlgebra.divOf_add {k : Type u_1} {G : Type u_2} [] (x : ) (a : G) (b : G) :
x.divOf (a + b) = (x.divOf a).divOf b
@[simp]
theorem AddMonoidAlgebra.divOfHom_apply_apply {k : Type u_1} {G : Type u_2} [] (g : ) (x : ) :
noncomputable def AddMonoidAlgebra.divOfHom {k : Type u_1} {G : Type u_2} [] :

A bundled version of AddMonoidAlgebra.divOf.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoidAlgebra.of'_mul_divOf {k : Type u_1} {G : Type u_2} [] (a : G) (x : ) :
( * x).divOf a = x
theorem AddMonoidAlgebra.mul_of'_divOf {k : Type u_1} {G : Type u_2} [] (x : ) (a : G) :
(x * ).divOf a = x
theorem AddMonoidAlgebra.of'_divOf {k : Type u_1} {G : Type u_2} [] (a : G) :
().divOf a = 1
noncomputable def AddMonoidAlgebra.modOf {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) :

The remainder upon division by of' k G g.

Equations
Instances For
@[simp]
theorem AddMonoidAlgebra.modOf_apply_of_not_exists_add {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) (g' : G) (h : ¬∃ (d : G), g' = g + d) :
(x.modOf g) g' = x g'
@[simp]
theorem AddMonoidAlgebra.modOf_apply_of_exists_add {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) (g' : G) (h : ∃ (d : G), g' = g + d) :
(x.modOf g) g' = 0
@[simp]
theorem AddMonoidAlgebra.modOf_apply_add_self {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) (d : G) :
(x.modOf g) (d + g) = 0
theorem AddMonoidAlgebra.modOf_apply_self_add {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) (d : G) :
(x.modOf g) (g + d) = 0
theorem AddMonoidAlgebra.of'_mul_modOf {k : Type u_1} {G : Type u_2} [] (g : G) (x : ) :
( * x).modOf g = 0
theorem AddMonoidAlgebra.mul_of'_modOf {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) :
(x * ).modOf g = 0
theorem AddMonoidAlgebra.of'_modOf {k : Type u_1} {G : Type u_2} [] (g : G) :
().modOf g = 0
theorem AddMonoidAlgebra.divOf_add_modOf {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) :
* x.divOf g + x.modOf g = x
theorem AddMonoidAlgebra.modOf_add_divOf {k : Type u_1} {G : Type u_2} [] (x : ) (g : G) :
x.modOf g + * x.divOf g = x
theorem AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero {k : Type u_1} {G : Type u_2} [] {x : } {g : G} :
x x.modOf g = 0