Documentation

Mathlib.Algebra.MonoidAlgebra.Division

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 #

Main results #

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

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

Equations
Instances For
    @[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) :
    (AddMonoidAlgebra.divOf x 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) :
    (AddMonoidAlgebra.divOf x g).support = Finset.preimage x.support (fun (x : G) => g + x) (_ : Set.InjOn (fun (x : G) => g + x) ((fun (x : G) => g + x) ⁻¹' x.support))
    @[simp]
    theorem AddMonoidAlgebra.zero_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) :
    @[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 = AddMonoidAlgebra.divOf x (Multiplicative.toAdd g)

    A bundled version of AddMonoidAlgebra.divOf.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def AddMonoidAlgebra.modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (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} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (g' : G) (h : ¬∃ (d : G), g' = g + d) :
        @[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) :
        @[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) :
        (AddMonoidAlgebra.modOf x 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) :
        (AddMonoidAlgebra.modOf x g) (g + d) = 0