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} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G

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

Equations

• x.divOf g = (Finsupp.comapDomain.addMonoidHom ⋯) x

@[simp]

theorem AddMonoidAlgebra.divOf_apply {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) (x : AddMonoidAlgebra k G) (g' : G) : (x.divOf g) g' = x (g + g')

@[simp]

theorem AddMonoidAlgebra.support_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) (x : AddMonoidAlgebra k G) : (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} [Semiring k] [AddCancelCommMonoid G] (g : G) : AddMonoidAlgebra.divOf 0 g = 0

@[simp]

theorem AddMonoidAlgebra.divOf_zero {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) : x.divOf 0 = x

theorem AddMonoidAlgebra.add_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (y : AddMonoidAlgebra k G) (g : G) : (x + y).divOf g = x.divOf g + y.divOf g

theorem AddMonoidAlgebra.divOf_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (a : G) (b : G) : x.divOf (a + b) = (x.divOf a).divOf b

noncomputable def AddMonoidAlgebra.divOfHom {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] : Multiplicative G →* AddMonoid.End (AddMonoidAlgebra k G)

A bundled version of AddMonoidAlgebra.divOf.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidAlgebra.divOfHom_apply_apply {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : Multiplicative G) (x : AddMonoidAlgebra k G) : (AddMonoidAlgebra.divOfHom g) x = x.divOf (Multiplicative.toAdd g)

theorem AddMonoidAlgebra.of'_mul_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (a : G) (x : AddMonoidAlgebra k G) : (AddMonoidAlgebra.of' k G a * x).divOf a = x

theorem AddMonoidAlgebra.mul_of'_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (a : G) : (x * AddMonoidAlgebra.of' k G a).divOf a = x

theorem AddMonoidAlgebra.of'_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (a : G) : (AddMonoidAlgebra.of' k G a).divOf a = 1

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

The remainder upon division by of' k G g.

Equations

• x.modOf g = Finsupp.filter (fun (g₁ : G) => ¬∃ (g₂ : G), g₁ = g + g₂) x

@[simp]

theorem AddMonoidAlgebra.modOf_apply_of_not_exists_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (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} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (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} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (d : G) : (x.modOf g) (d + g) = 0

theorem AddMonoidAlgebra.modOf_apply_self_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (d : G) : (x.modOf g) (g + d) = 0

theorem AddMonoidAlgebra.of'_mul_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) (x : AddMonoidAlgebra k G) : (AddMonoidAlgebra.of' k G g * x).modOf g = 0

theorem AddMonoidAlgebra.mul_of'_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : (x * AddMonoidAlgebra.of' k G g).modOf g = 0

theorem AddMonoidAlgebra.of'_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) : (AddMonoidAlgebra.of' k G g).modOf g = 0

theorem AddMonoidAlgebra.divOf_add_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra.of' k G g * x.divOf g + x.modOf g = x

theorem AddMonoidAlgebra.modOf_add_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : x.modOf g + AddMonoidAlgebra.of' k G g * x.divOf g = x

theorem AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] {x : AddMonoidAlgebra k G} {g : G} : AddMonoidAlgebra.of' k G g ∣ x ↔ x.modOf g = 0