# mathlib3documentation

algebra.monoid_algebra.division

# Division of add_monoid_algebra by monomials #

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

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

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

## Main definitions #

• add_monoid_algebra.div_of x g: divides x by the monomial add_monoid_algebra.of k G g
• add_monoid_algebra.mod_of x g: the remainder upon dividing x by the monomial add_monoid_algebra.of k G g.

## Main results #

• add_monoid_algebra.div_of_add_mod_of, add_monoid_algebra.mod_of_add_div_of: div_of and mod_of 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 semigroup_has_dvd. The results in this file could be duplicated for monoid_algebra by using g ∣ g', but this can't be done automatically, and in any case is not likely to be very useful.

noncomputable def add_monoid_algebra.div_of {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g : G) :

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

Equations
@[simp]
theorem add_monoid_algebra.div_of_apply {k : Type u_1} {G : Type u_2} [semiring k] (g : G) (x : G) (g' : G) :
(x.div_of g) g' = x (g + g')
@[simp]
theorem add_monoid_algebra.support_div_of {k : Type u_1} {G : Type u_2} [semiring k] (g : G) (x : G) :
@[simp]
theorem add_monoid_algebra.zero_div_of {k : Type u_1} {G : Type u_2} [semiring k] (g : G) :
0.div_of g = 0
@[simp]
theorem add_monoid_algebra.div_of_zero {k : Type u_1} {G : Type u_2} [semiring k] (x : G) :
x.div_of 0 = x
theorem add_monoid_algebra.add_div_of {k : Type u_1} {G : Type u_2} [semiring k] (x y : G) (g : G) :
(x + y).div_of g = x.div_of g + y.div_of g
theorem add_monoid_algebra.div_of_add {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (a b : G) :
x.div_of (a + b) = (x.div_of a).div_of b
@[simp]
theorem add_monoid_algebra.div_of_hom_apply_apply {k : Type u_1} {G : Type u_2} [semiring k] (g : multiplicative G) (x : G) :
noncomputable def add_monoid_algebra.div_of_hom {k : Type u_1} {G : Type u_2} [semiring k]  :

A bundled version of add_monoid_algebra.div_of.

Equations
theorem add_monoid_algebra.of'_mul_div_of {k : Type u_1} {G : Type u_2} [semiring k] (a : G) (x : G) :
a * x).div_of a = x
theorem add_monoid_algebra.mul_of'_div_of {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (a : G) :
(x * a).div_of a = x
theorem add_monoid_algebra.of'_div_of {k : Type u_1} {G : Type u_2} [semiring k] (a : G) :
a).div_of a = 1
noncomputable def add_monoid_algebra.mod_of {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g : G) :

The remainder upon division by of' k G g.

Equations
@[simp]
theorem add_monoid_algebra.mod_of_apply_of_not_exists_add {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g g' : G) (h : ¬ (d : G), g' = g + d) :
(x.mod_of g) g' = x g'
@[simp]
theorem add_monoid_algebra.mod_of_apply_of_exists_add {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g g' : G) (h : (d : G), g' = g + d) :
(x.mod_of g) g' = 0
@[simp]
theorem add_monoid_algebra.mod_of_apply_add_self {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g d : G) :
(x.mod_of g) (d + g) = 0
@[simp]
theorem add_monoid_algebra.mod_of_apply_self_add {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g d : G) :
(x.mod_of g) (g + d) = 0
theorem add_monoid_algebra.of'_mul_mod_of {k : Type u_1} {G : Type u_2} [semiring k] (g : G) (x : G) :
g * x).mod_of g = 0
theorem add_monoid_algebra.mul_of'_mod_of {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g : G) :
(x * g).mod_of g = 0
theorem add_monoid_algebra.of'_mod_of {k : Type u_1} {G : Type u_2} [semiring k] (g : G) :
g).mod_of g = 0
theorem add_monoid_algebra.div_of_add_mod_of {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g : G) :
* x.div_of g + x.mod_of g = x
theorem add_monoid_algebra.mod_of_add_div_of {k : Type u_1} {G : Type u_2} [semiring k] (x : G) (g : G) :
x.mod_of g + * x.div_of g = x
theorem add_monoid_algebra.of'_dvd_iff_mod_of_eq_zero {k : Type u_1} {G : Type u_2} [semiring k] {x : G} {g : G} :
x x.mod_of g = 0