mathlib3 documentation

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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k G) (g : G) :

add_monoid_algebra k G

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

Equations

x.div_of g = ⇑(finsupp.comap_domain.add_monoid_hom _) x

@[simp]

theorem add_monoid_algebra.div_of_apply {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (g : G) (x : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (g : G) (x : add_monoid_algebra k G) :

(x.div_of g).support = x.support.preimage (has_add.add g) _

@[simp]

theorem add_monoid_algebra.zero_div_of {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k G) :

x.div_of 0 = x

theorem add_monoid_algebra.add_div_of {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (x y : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (g : multiplicative G) (x : add_monoid_algebra k G) :

⇑(⇑add_monoid_algebra.div_of_hom g) x = x.div_of (⇑multiplicative.to_add g)

noncomputable def add_monoid_algebra.div_of_hom {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] :

multiplicative G →* add_monoid.End (add_monoid_algebra k G)

A bundled version of add_monoid_algebra.div_of.

Equations

add_monoid_algebra.div_of_hom = {to_fun := λ (g : multiplicative G), {to_fun := λ (x : add_monoid_algebra k G), x.div_of (⇑multiplicative.to_add g), map_zero' := _, map_add' := _}, map_one' := _, map_mul' := _}

theorem add_monoid_algebra.of'_mul_div_of {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (a : G) (x : add_monoid_algebra k G) :

(add_monoid_algebra.of' k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k G) (a : G) :

(x * add_monoid_algebra.of' k G a).div_of a = x

theorem add_monoid_algebra.of'_div_of {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (a : G) :

(add_monoid_algebra.of' k G a).div_of a = 1

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

add_monoid_algebra k G

The remainder upon division by of' k G g.

Equations

x.mod_of g = finsupp.filter (λ (g₁ : G), ¬∃ (g₂ : G), g₁ = g + g₂) x

@[simp]

theorem add_monoid_algebra.mod_of_apply_of_not_exists_add {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (x : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k 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] [add_cancel_comm_monoid G] (g : G) (x : add_monoid_algebra k G) :

(add_monoid_algebra.of' k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k G) (g : G) :

(x * add_monoid_algebra.of' k G g).mod_of g = 0

theorem add_monoid_algebra.of'_mod_of {k : Type u_1} {G : Type u_2} [semiring k] [add_cancel_comm_monoid G] (g : G) :

(add_monoid_algebra.of' k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k G) (g : G) :

add_monoid_algebra.of' k 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] [add_cancel_comm_monoid G] (x : add_monoid_algebra k G) (g : G) :

x.mod_of g + add_monoid_algebra.of' k G 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] [add_cancel_comm_monoid G] {x : add_monoid_algebra k G} {g : G} :

add_monoid_algebra.of' k G g ∣ x ↔ x.mod_of g = 0