[Merged by Bors] - feat: port Algebra.MonoidAlgebra.Division

Mathlib.lean

@@ -146,6 +146,7 @@ import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Module.ULift
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Algebra.MonoidAlgebra.Degree
+import Mathlib.Algebra.MonoidAlgebra.Division
 import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Algebra.NeZero

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.monoid_algebra.basic
-! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
+! leanprover-community/mathlib commit 57e09a1296bfb4330ddf6624f1028ba186117d82
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -563,6 +563,19 @@ theorem mul_single_one_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x
   f.mul_single_apply_aux fun a => by rw [mul_one]
 #align monoid_algebra.mul_single_one_apply MonoidAlgebra.mul_single_one_apply
 
+theorem mul_single_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
+    (h : ¬∃ d, g' = d * g) : (x * single g r) g' = 0 := by
+  classical
+    rw [mul_apply, Finsupp.sum_comm, Finsupp.sum_single_index]
+    swap
+    · simp_rw [Finsupp.sum, MulZeroClass.mul_zero, ite_self, Finset.sum_const_zero]
+    · apply Finset.sum_eq_zero
+      simp_rw [ite_eq_right_iff]
+      rintro g'' _hg'' rfl
+      exfalso
+      exact h ⟨_, rfl⟩
+#align monoid_algebra.mul_single_apply_of_not_exists_mul MonoidAlgebra.mul_single_apply_of_not_exists_mul
+
 theorem single_mul_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
     (H : ∀ a, x * a = y ↔ a = z) : (single x r * f) y = r * f z := by
   classical exact
@@ -582,6 +595,19 @@ theorem single_one_mul_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x
   f.single_mul_apply_aux fun a => by rw [one_mul]
 #align monoid_algebra.single_one_mul_apply MonoidAlgebra.single_one_mul_apply
 
+theorem single_mul_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
+    (h : ¬∃ d, g' = g * d) : (single g r * x) g' = 0 := by
+  classical
+    rw [mul_apply, Finsupp.sum_single_index]
+    swap
+    · simp_rw [Finsupp.sum, MulZeroClass.zero_mul, ite_self, Finset.sum_const_zero]
+    · apply Finset.sum_eq_zero
+      simp_rw [ite_eq_right_iff]
+      rintro g'' _hg'' rfl
+      exfalso
+      exact h ⟨_, rfl⟩
+#align monoid_algebra.single_mul_apply_of_not_exists_mul MonoidAlgebra.single_mul_apply_of_not_exists_mul
+
 theorem liftNC_smul [MulOneClass G] {R : Type _} [Semiring R] (f : k →+* R) (g : G →* R) (c : k)
     (φ : MonoidAlgebra k G) : liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ := by
   suffices :
@@ -1611,6 +1637,11 @@ theorem mul_single_zero_apply [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k
   f.mul_single_apply_aux r _ _ _ fun a => by rw [add_zero]
 #align add_monoid_algebra.mul_single_zero_apply AddMonoidAlgebra.mul_single_zero_apply
 
+theorem mul_single_apply_of_not_exists_add [Add G] (r : k) {g g' : G} (x : AddMonoidAlgebra k G)
+    (h : ¬∃ d, g' = d + g) : (x * single g r) g' = 0 :=
+  @MonoidAlgebra.mul_single_apply_of_not_exists_mul k (Multiplicative G) _ _ _ _ _ _ h
+#align add_monoid_algebra.mul_single_apply_of_not_exists_add AddMonoidAlgebra.mul_single_apply_of_not_exists_add
+
 theorem single_mul_apply_aux [Add G] (f : AddMonoidAlgebra k G) (r : k) (x y z : G)
     (H : ∀ a, x + a = y ↔ a = z) : (single x r * f) y = r * f z :=
   @MonoidAlgebra.single_mul_apply_aux k (Multiplicative G) _ _ _ _ _ _ _ H
@@ -1621,6 +1652,11 @@ theorem single_zero_mul_apply [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k
   f.single_mul_apply_aux r _ _ _ fun a => by rw [zero_add]
 #align add_monoid_algebra.single_zero_mul_apply AddMonoidAlgebra.single_zero_mul_apply
 
+theorem single_mul_apply_of_not_exists_add [Add G] (r : k) {g g' : G} (x : AddMonoidAlgebra k G)
+    (h : ¬∃ d, g' = g + d) : (single g r * x) g' = 0 :=
+  @MonoidAlgebra.single_mul_apply_of_not_exists_mul k (Multiplicative G) _ _ _ _ _ _ h
+#align add_monoid_algebra.single_mul_apply_of_not_exists_add AddMonoidAlgebra.single_mul_apply_of_not_exists_add
+
 theorem mul_single_apply [AddGroup G] (f : AddMonoidAlgebra k G) (r : k) (x y : G) :
     (f * single x r) y = f (y - x) * r :=
   (sub_eq_add_neg y x).symm ▸ @MonoidAlgebra.mul_single_apply k (Multiplicative G) _ _ _ _ _ _

Mathlib/Algebra/MonoidAlgebra/Division.lean

@@ -0,0 +1,203 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module algebra.monoid_algebra.division
+! leanprover-community/mathlib commit 57e09a1296bfb4330ddf6624f1028ba186117d82
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Data.Finsupp.Order
+
+/-!
+# 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 `LaurentPolynomial`s), 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.
+
+-/
+
+
+variable {k G : Type _} [Semiring k]
+
+namespace AddMonoidAlgebra
+
+section
+
+variable [AddCancelCommMonoid G]
+
+/-- Divide by `of' k G g`, discarding terms not divisible by this. -/
+noncomputable def divOf (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G :=
+  -- note: comapping by `+ g` has the effect of subtracting `g` from every element in
+  -- the support, and discarding the elements of the support from which `g` can't be subtracted.
+  -- If `G` is an additive group, such as `ℤ` when used for `LaurentPolynomial`,
+  -- then no discarding occurs.
+  @Finsupp.comapDomain.addMonoidHom _ _ _ _ ((· + ·) g) (add_right_injective g) x
+#align add_monoid_algebra.div_of AddMonoidAlgebra.divOf
+
+local infixl:70 " /ᵒᶠ " => divOf
+
+@[simp]
+theorem divOf_apply (g : G) (x : AddMonoidAlgebra k G) (g' : G) : (x /ᵒᶠ g) g' = x (g + g') :=
+  rfl
+#align add_monoid_algebra.div_of_apply AddMonoidAlgebra.divOf_apply
+
+@[simp]
+theorem support_divOf (g : G) (x : AddMonoidAlgebra k G) :
+    (x /ᵒᶠ g).support =
+      x.support.preimage ((· + ·) g) (Function.Injective.injOn (add_right_injective g) _) :=
+  rfl
+#align add_monoid_algebra.support_div_of AddMonoidAlgebra.support_divOf
+
+@[simp]
+theorem zero_divOf (g : G) : (0 : AddMonoidAlgebra k G) /ᵒᶠ g = 0 :=
+  map_zero _
+#align add_monoid_algebra.zero_div_of AddMonoidAlgebra.zero_divOf
+
+@[simp]
+theorem divOf_zero (x : AddMonoidAlgebra k G) : x /ᵒᶠ 0 = x := by
+  apply Finsupp.ext
+  intro
+  simp only [AddMonoidAlgebra.divOf_apply, zero_add]
+#align add_monoid_algebra.div_of_zero AddMonoidAlgebra.divOf_zero
+
+theorem add_divOf (x y : AddMonoidAlgebra k G) (g : G) : (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g :=
+  map_add _ _ _
+#align add_monoid_algebra.add_div_of AddMonoidAlgebra.add_divOf
+
+theorem divOf_add (x : AddMonoidAlgebra k G) (a b : G) : x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b := by
+  apply Finsupp.ext
+  intro
+  simp only [AddMonoidAlgebra.divOf_apply, add_assoc]
+#align add_monoid_algebra.div_of_add AddMonoidAlgebra.divOf_add
+
+/-- A bundled version of `AddMonoidAlgebra.divOf`. -/
+@[simps]
+noncomputable def divOfHom : Multiplicative G →* AddMonoid.End (AddMonoidAlgebra k G) where
+  toFun g :=
+    { toFun := fun x => divOf x g.toAdd
+      map_zero' := zero_divOf _
+      map_add' := fun x y => add_divOf x y g.toAdd }
+  map_one' := AddMonoidHom.ext divOf_zero
+  map_mul' g₁ g₂ :=
+    AddMonoidHom.ext fun x => (congr_arg _ (add_comm g₁.toAdd g₂.toAdd)).trans (divOf_add _ _ _)
+#align add_monoid_algebra.div_of_hom AddMonoidAlgebra.divOfHom
+
+theorem of'_mul_divOf (a : G) (x : AddMonoidAlgebra k G) : of' k G a * x /ᵒᶠ a = x := by
+  apply Finsupp.ext
+  intro
+  rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
+  intro c
+  exact add_right_inj _
+#align add_monoid_algebra.of'_mul_div_of AddMonoidAlgebra.of'_mul_divOf
+
+theorem mul_of'_divOf (x : AddMonoidAlgebra k G) (a : G) : x * of' k G a /ᵒᶠ a = x := by
+  apply Finsupp.ext
+  intro
+  rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
+  intro c
+  rw [add_comm]
+  exact add_right_inj _
+#align add_monoid_algebra.mul_of'_div_of AddMonoidAlgebra.mul_of'_divOf
+
+theorem of'_divOf (a : G) : of' k G a /ᵒᶠ a = 1 := by
+  simpa only [one_mul] using mul_of'_divOf (1 : AddMonoidAlgebra k G) a
+#align add_monoid_algebra.of'_div_of AddMonoidAlgebra.of'_divOf
+
+/-- The remainder upon division by `of' k G g`. -/
+noncomputable def modOf (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G :=
+  x.filter fun g₁ => ¬∃ g₂, g₁ = g + g₂
+#align add_monoid_algebra.mod_of AddMonoidAlgebra.modOf
+
+local infixl:70 " %ᵒᶠ " => modOf
+
+@[simp]
+theorem modOf_apply_of_not_exists_add (x : AddMonoidAlgebra k G) (g : G) (g' : G)
+    (h : ¬∃ d, g' = g + d) : (x %ᵒᶠ g) g' = x g' :=
+  Finsupp.filter_apply_pos _ _ h
+#align add_monoid_algebra.mod_of_apply_of_not_exists_add AddMonoidAlgebra.modOf_apply_of_not_exists_add
+
+@[simp]
+theorem modOf_apply_of_exists_add (x : AddMonoidAlgebra k G) (g : G) (g' : G)
+    (h : ∃ d, g' = g + d) : (x %ᵒᶠ g) g' = 0 :=
+  Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]
+#align add_monoid_algebra.mod_of_apply_of_exists_add AddMonoidAlgebra.modOf_apply_of_exists_add
+
+@[simp]
+theorem modOf_apply_add_self (x : AddMonoidAlgebra k G) (g : G) (d : G) : (x %ᵒᶠ g) (d + g) = 0 :=
+  modOf_apply_of_exists_add _ _ _ ⟨_, add_comm _ _⟩
+#align add_monoid_algebra.mod_of_apply_add_self AddMonoidAlgebra.modOf_apply_add_self
+
+@[simp]
+theorem modOf_apply_self_add (x : AddMonoidAlgebra k G) (g : G) (d : G) : (x %ᵒᶠ g) (g + d) = 0 :=
+  modOf_apply_of_exists_add _ _ _ ⟨_, rfl⟩
+#align add_monoid_algebra.mod_of_apply_self_add AddMonoidAlgebra.modOf_apply_self_add
+
+theorem of'_mul_modOf (g : G) (x : AddMonoidAlgebra k G) : of' k G g * x %ᵒᶠ g = 0 := by
+  apply Finsupp.ext
+  intro g'
+  rw [Finsupp.zero_apply]
+  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
+  · rw [modOf_apply_self_add]
+  · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
+#align add_monoid_algebra.of'_mul_mod_of AddMonoidAlgebra.of'_mul_modOf
+
+theorem mul_of'_modOf (x : AddMonoidAlgebra k G) (g : G) : x * of' k G g %ᵒᶠ g = 0 := by
+  apply Finsupp.ext
+  intro g'
+  rw [Finsupp.zero_apply]
+  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
+  · rw [modOf_apply_self_add]
+  · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]
+    simpa only [add_comm] using h
+#align add_monoid_algebra.mul_of'_mod_of AddMonoidAlgebra.mul_of'_modOf
+
+theorem of'_modOf (g : G) : of' k G g %ᵒᶠ g = 0 := by
+  simpa only [one_mul] using mul_of'_modOf (1 : AddMonoidAlgebra k G) g
+#align add_monoid_algebra.of'_mod_of AddMonoidAlgebra.of'_modOf
+
+theorem divOf_add_modOf (x : AddMonoidAlgebra k G) (g : G) :
+    of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x := by
+  apply Finsupp.ext
+  intro g'
+  simp_rw [Finsupp.add_apply]
+  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
+  swap
+  · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
+      zero_add]
+  · rw [modOf_apply_self_add, add_zero]
+    rw [of'_apply, single_mul_apply_aux _ _ _, one_mul, div_of_apply]
+    intro a
+    exact add_right_inj _
+#align add_monoid_algebra.div_of_add_mod_of AddMonoidAlgebra.divOf_add_modOf
+
+theorem modOf_add_divOf (x : AddMonoidAlgebra k G) (g : G) : x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x :=
+  by rw [add_comm, divOf_add_modOf]
+#align add_monoid_algebra.mod_of_add_div_of AddMonoidAlgebra.modOf_add_divOf
+
+end
+
+end AddMonoidAlgebra

Mathlib/Data/Polynomial/Inductions.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Damiano Testa, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module data.polynomial.inductions
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 57e09a1296bfb4330ddf6624f1028ba186117d82
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathlib.Algebra.MonoidAlgebra.Division
 import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Polynomial.Degree.Definitions
 import Mathlib.Data.Polynomial.Induction
@@ -38,17 +39,15 @@ variable [Semiring R] {p q : R[X]}
 /-- `divX p` returns a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
   It can be used in a semiring where the usual division algorithm is not possible -/
 def divX (p : R[X]) : R[X] :=
-  ∑ n in Ico 0 p.natDegree, monomial n (p.coeff (n + 1))
+  ⟨AddMonoidAlgebra.divOf p.toFinsupp 1⟩
 set_option linter.uppercaseLean3 false in
 #align polynomial.div_X Polynomial.divX
 
 @[simp]
 theorem coeff_divX : (divX p).coeff n = p.coeff (n + 1) := by
-  simp only [divX, coeff_monomial, true_and_iff, finset_sum_coeff, not_lt, mem_Ico, zero_le,
-    Finset.sum_ite_eq', ite_eq_left_iff]
-  intro h
-  rw [coeff_eq_zero_of_natDegree_lt (Nat.lt_succ_of_le h)]
-set_option linter.uppercaseLean3 false in
+  rw [add_comm]
+  cases p
+  rfl
 #align polynomial.coeff_div_X Polynomial.coeff_divX
 
 theorem divX_mul_X_add (p : R[X]) : divX p * X + C (p.coeff 0) = p :=
@@ -58,7 +57,7 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem divX_C (a : R) : divX (C a) = 0 :=
-  ext fun n => by simp [divX, coeff_C]
+  ext fun n => by simp [coeff_divX, coeff_C, Finsupp.single_eq_of_ne _]
 set_option linter.uppercaseLean3 false in
 #align polynomial.div_X_C Polynomial.divX_C