Merge remote-tracking branch 'origin/master' into MultilinearMapContDiff

Archive/Imo/Imo1962Q1.lean

@@ -117,11 +117,10 @@ theorem case_more_digits {c n : ℕ} (h1 : (digits 10 c).length ≥ 6) (h2 : Pro
     intro h4
     have h5 : (digits 10 c).length = 0 := by simp [h4]
     exact case_0_digit h5 h2
-  have h6 : 2 ≤ 10 := by decide
   calc
     n ≥ 10 * c := le.intro h2.left.symm
-    _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c h6 h3)
-    _ ≥ 10 ^ 6 := ((pow_le_iff_le_right h6).mpr h1)
+    _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c (by decide) h3)
+    _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) h1
     _ ≥ 153846 := by norm_num
 #align imo1962_q1.case_more_digits Imo1962Q1.case_more_digits
 

Archive/Imo/Imo1969Q1.lean

@@ -86,7 +86,7 @@ theorem aChoice_good (b : ℕ) : aChoice b ∈ goodNats :=
 /-- `aChoice` is a strictly monotone function; this is easily proven by chaining together lemmas
 in the `strictMono` namespace. -/
 theorem aChoice_strictMono : StrictMono aChoice :=
-  ((strictMono_id.const_add 2).nat_pow (by decide : 0 < 4)).const_mul (by decide : 0 < 4)
+  ((strictMono_id.const_add 2).nat_pow (by decide)).const_mul (by decide)
 #align imo1969_q1.a_choice_strict_mono Imo1969Q1.aChoice_strictMono
 
 end Imo1969Q1

Archive/Imo/Imo2001Q2.lean

@@ -41,7 +41,7 @@ theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
       = a ^ 3 * (a * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)) := by ring
     _ ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4) := ?_
   gcongr
-  apply le_of_pow_le_pow _ (by positivity) zero_lt_two
+  apply le_of_pow_le_pow_left two_ne_zero (by positivity)
   rw [mul_pow, sq_sqrt (by positivity), ← sub_nonneg]
   calc
     (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
@@ -67,7 +67,7 @@ open Imo2001Q2
 theorem imo2001_q2 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : ↑1 ≤
     a / sqrt (a ^ 2 + ↑8 * b * c) + b / sqrt (b ^ 2 + ↑8 * c * a) + c / sqrt (c ^ 2 + ↑8 * a * b) :=
   have h3 : ∀ {x : ℝ}, 0 < x → (x ^ (3 : ℝ)⁻¹) ^ 3 = x := fun hx =>
-    show ↑3 = (3 : ℝ) by norm_num ▸ rpow_nat_inv_pow_nat hx.le three_ne_zero
+    show ↑3 = (3 : ℝ) by norm_num ▸ rpow_inv_natCast_pow hx.le three_ne_zero
   calc
     1 ≤ _ := imo2001_q2' (rpow_pos_of_pos ha _) (rpow_pos_of_pos hb _) (rpow_pos_of_pos hc _)
     _ = _ := by rw [h3 ha, h3 hb, h3 hc]

Archive/Imo/Imo2006Q3.lean

@@ -71,7 +71,7 @@ theorem subst_wlog {x y z s : ℝ} (hxy : 0 ≤ x * y) (hxyz : x + y + z = 0) :
       _ ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4 := by
           gcongr (?_ + _) ^ 4 / _
           apply rhs_ineq
-  refine le_of_pow_le_pow 2 (by positivity) (by positivity) ?_
+  refine le_of_pow_le_pow_left two_ne_zero (by positivity) ?_
   calc
     (32 * |x * y * z * s|) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)) := by
       rw [mul_pow, sq_abs, hz]; ring

Archive/Imo/Imo2008Q3.lean

@@ -62,10 +62,10 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hreal₂ : (p : ℝ) > 20 := by assumption_mod_cast
   have hreal₃ : (k : ℝ) ^ 2 + 4 ≥ p := by assumption_mod_cast
   have hreal₅ : (k : ℝ) > 4 := by
-    refine' lt_of_pow_lt_pow 2 k.cast_nonneg _
+    refine' lt_of_pow_lt_pow_left 2 k.cast_nonneg _
     linarith only [hreal₂, hreal₃]
   have hreal₆ : (k : ℝ) > sqrt (2 * n) := by
-    refine' lt_of_pow_lt_pow 2 k.cast_nonneg _
+    refine' lt_of_pow_lt_pow_left 2 k.cast_nonneg _
     rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
     linarith only [hreal₁, hreal₃, hreal₅]
   exact ⟨n, hnat₁, by linarith only [hreal₆, hreal₁]⟩

Archive/Imo/Imo2008Q4.lean

@@ -29,8 +29,7 @@ open Real
 namespace Imo2008Q4
 
 theorem abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : |x| = 1 := by
-  rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_pow, pow_abs, h,
-    abs_one]
+  rw [← pow_left_inj (abs_nonneg x) zero_le_one hn, one_pow, pow_abs, h, abs_one]
 #align imo2008_q4.abs_eq_one_of_pow_eq_one Imo2008Q4.abs_eq_one_of_pow_eq_one
 
 end Imo2008Q4

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -126,7 +126,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
     have hfa : 0 ≤ f a := by
       -- Porting note: was `simp_rw`
       simp only [hf, ← sq]
-      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow ha _)) _ <;> norm_num
+      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha _)) _ <;> norm_num
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (Set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (Set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩
@@ -137,7 +137,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
           norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
-          refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
+          refine' add_le_add (sub_le_sub_left (pow_le_pow_right ha _) _) _ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
     have ha' := neg_nonpos.mpr (hle.trans ha)

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -115,7 +115,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p
       | .succ k =>
         apply ne_of_lt _ jcon2
         rw [mersenne, ← Nat.pred_eq_sub_one, Nat.lt_pred_iff, ← pow_one (Nat.succ 1)]
-        apply pow_lt_pow (Nat.lt_succ_self 1) (Nat.succ_lt_succ (Nat.succ_pos k))
+        apply pow_lt_pow_right (Nat.lt_succ_self 1) (Nat.succ_lt_succ (Nat.succ_pos k))
     contrapose! hm
     simp [hm]
 #align theorems_100.nat.eq_two_pow_mul_prime_mersenne_of_even_perfect Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -168,7 +168,7 @@ theorem card_le_two_pow {x k : ℕ} :
     card M₁ ≤ card (image f K) := card_le_of_subset h
     _ ≤ card K := card_image_le
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [card_powerset]; rfl
-    _ ≤ 2 ^ card (range k) := (pow_le_pow one_le_two card_image_le)
+    _ ≤ 2 ^ card (range k) := (pow_le_pow_right one_le_two card_image_le)
     _ = 2 ^ k := by rw [card_range k]
 #align theorems_100.card_le_two_pow Theorems100.card_le_two_pow
 

Archive/ZagierTwoSquares.lean

@@ -195,5 +195,5 @@ theorem Nat.Prime.sq_add_sq' {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) :
     (Equiv.Perm.card_fixedPoints_modEq (p := 2) (n := 1) (complexInvo_sq k))
   contrapose key
   rw [Set.not_nonempty_iff_eq_empty] at key
-  simp_rw [key, Fintype.card_of_isEmpty, card_fixedPoints_eq_one]
+  simp_rw [key, Fintype.card_eq_zero, card_fixedPoints_eq_one]
   decide

Counterexamples.lean

@@ -8,6 +8,7 @@ import Counterexamples.HomogeneousPrimeNotPrime
 import Counterexamples.LinearOrderWithPosMulPosEqZero
 import Counterexamples.MapFloor
 import Counterexamples.Monic_nonRegular
+import Counterexamples.OrderedCancelAddCommMonoidWithBounds
 import Counterexamples.Phillips
 import Counterexamples.Pseudoelement
 import Counterexamples.QuadraticForm

Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2023 Martin Dvorak. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Dvorak
+-/
+import Mathlib.Algebra.Order.Monoid.Defs
+
+/-!
+# Do not combine OrderedCancelAddCommMonoid with BoundedOrder
+
+This file shows that combining `OrderedCancelAddCommMonoid` with `BoundedOrder` is not a good idea,
+as such a structure must be trivial (`⊥ = x = ⊤` for all `x`).
+The same applies to any superclasses, e.g. combining `StrictOrderedSemiring` with `CompleteLattice`.
+-/
+
+example {α : Type*} [OrderedCancelAddCommMonoid α] [BoundedOrder α] [Nontrivial α] : False :=
+  have top_pos := pos_of_lt_add_right (bot_le.trans_lt (add_lt_add_left bot_lt_top (⊥ : α)))
+  have top_add_top_lt_self := lt_add_of_le_of_pos (@le_top _ _ _ (⊤ + ⊤)) top_pos
+  top_add_top_lt_self.false

Mathlib.lean

@@ -377,6 +377,7 @@ import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.LatticeGroup
 import Mathlib.Algebra.Order.Module
+import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
@@ -870,6 +871,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Base
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 import Mathlib.Analysis.SpecialFunctions.Log.Monotone
+import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.Analysis.SpecialFunctions.NonIntegrable
 import Mathlib.Analysis.SpecialFunctions.PolarCoord
 import Mathlib.Analysis.SpecialFunctions.PolynomialExp
@@ -2059,6 +2061,7 @@ import Mathlib.FieldTheory.Laurent
 import Mathlib.FieldTheory.Minpoly.Basic
 import Mathlib.FieldTheory.Minpoly.Field
 import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
+import Mathlib.FieldTheory.Minpoly.MinpolyDiv
 import Mathlib.FieldTheory.MvPolynomial
 import Mathlib.FieldTheory.Normal
 import Mathlib.FieldTheory.NormalClosure
@@ -2115,6 +2118,7 @@ import Mathlib.Geometry.Manifold.Diffeomorph
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.Geometry.Manifold.Instances.Sphere
 import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
+import Mathlib.Geometry.Manifold.InteriorBoundary
 import Mathlib.Geometry.Manifold.LocalInvariantProperties
 import Mathlib.Geometry.Manifold.MFDeriv
 import Mathlib.Geometry.Manifold.Metrizable
@@ -2355,6 +2359,7 @@ import Mathlib.LinearAlgebra.CliffordAlgebra.Even
 import Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
 import Mathlib.LinearAlgebra.CliffordAlgebra.Fold
 import Mathlib.LinearAlgebra.CliffordAlgebra.Grading
+import Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
 import Mathlib.LinearAlgebra.CliffordAlgebra.Star
 import Mathlib.LinearAlgebra.Coevaluation
 import Mathlib.LinearAlgebra.Contraction
@@ -2475,6 +2480,8 @@ import Mathlib.LinearAlgebra.TensorAlgebra.Grading
 import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 import Mathlib.LinearAlgebra.TensorPower
 import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Graded.External
+import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
 import Mathlib.LinearAlgebra.TensorProduct.Opposite
 import Mathlib.LinearAlgebra.TensorProduct.Prod
@@ -2920,6 +2927,7 @@ import Mathlib.Order.RelSeries
 import Mathlib.Order.SemiconjSup
 import Mathlib.Order.Sublattice
 import Mathlib.Order.SuccPred.Basic
+import Mathlib.Order.SuccPred.CompleteLinearOrder
 import Mathlib.Order.SuccPred.IntervalSucc
 import Mathlib.Order.SuccPred.Limit
 import Mathlib.Order.SuccPred.LinearLocallyFinite
@@ -3065,6 +3073,7 @@ import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.IntegralClosure
 import Mathlib.RingTheory.IntegralDomain
+import Mathlib.RingTheory.IntegralRestrict
 import Mathlib.RingTheory.IntegrallyClosed
 import Mathlib.RingTheory.IsAdjoinRoot
 import Mathlib.RingTheory.IsTensorProduct

Mathlib/Algebra/Algebra/Basic.lean

@@ -924,3 +924,27 @@ end Module
 example {R A} [CommSemiring R] [Semiring A] [Module R A] [SMulCommClass R A A]
     [IsScalarTower R A A] : Algebra R A :=
   Algebra.ofModule smul_mul_assoc mul_smul_comm
+
+section invertibility
+
+variable {R A B : Type*}
+variable [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
+
+/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
+invertible when `algebraMap R A r` is. -/
+abbrev Invertible.algebraMapOfInvertibleAlgebraMap (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R}
+    (h : Invertible (algebraMap R A r)) : Invertible (algebraMap R B r) where
+  invOf := f ⅟(algebraMap R A r)
+  invOf_mul_self := by rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
+    mul_invOf_self, hf]
+  mul_invOf_self := by rw [← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]
+
+/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
+a unit when `algebraMap R A r` is. -/
+lemma IsUnit.algebraMap_of_algebraMap (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R}
+    (h : IsUnit (algebraMap R A r)) : IsUnit (algebraMap R B r) :=
+  let ⟨i⟩ := nonempty_invertible h
+  letI := Invertible.algebraMapOfInvertibleAlgebraMap f hf i
+  isUnit_of_invertible _
+
+end invertibility

Mathlib/Algebra/CharP/Basic.lean

@@ -145,12 +145,30 @@ theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b
   rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
 #align char_p.int_cast_eq_int_cast CharP.intCast_eq_intCast
 
-theorem CharP.natCast_eq_natCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} :
-    (a : R) = b ↔ a ≡ b [MOD p] := by
-  rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
-  exact (CharP.intCast_eq_intCast _ _).trans Int.coe_nat_modEq_iff
+theorem CharP.natCast_eq_natCast' [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}
+    (h : a ≡ b [MOD p]) : (a : R) = b := by
+  wlog hle : a ≤ b
+  · exact (this R p h.symm (le_of_not_le hle)).symm
+  rw [Nat.modEq_iff_dvd' hle] at h
+  rw [← Nat.sub_add_cancel hle, Nat.cast_add, (CharP.cast_eq_zero_iff R p _).mpr h, zero_add]
+
+theorem CharP.natCast_eq_natCast [AddMonoidWithOne R] [IsRightCancelAdd R] (p : ℕ) [CharP R p]
+    {a b : ℕ} : (a : R) = b ↔ a ≡ b [MOD p] := by
+  wlog hle : a ≤ b
+  · rw [eq_comm, this R p (le_of_not_le hle), Nat.ModEq.comm]
+  rw [Nat.modEq_iff_dvd' hle, ← CharP.cast_eq_zero_iff R p (b - a),
+    ← add_right_cancel_iff (G := R) (a := a) (b := b - a), zero_add, ← Nat.cast_add,
+    Nat.sub_add_cancel hle, eq_comm]
 #align char_p.nat_cast_eq_nat_cast CharP.natCast_eq_natCast
 
+theorem CharP.intCast_eq_intCast_mod [AddGroupWithOne R] (p : ℕ) [CharP R p] {a : ℤ} :
+    (a : R) = a % (p : ℤ) :=
+  (CharP.intCast_eq_intCast R p).mpr (Int.mod_modEq a p).symm
+
+theorem CharP.natCast_eq_natCast_mod [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a : ℕ} :
+    (a : R) = a % p :=
+  CharP.natCast_eq_natCast' R p (Nat.mod_modEq a p).symm
+
 theorem CharP.eq [AddMonoidWithOne R] {p q : ℕ} (_c1 : CharP R p) (_c2 : CharP R q) : p = q :=
   Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R p q).1 (CharP.cast_eq_zero _ _))
     ((CharP.cast_eq_zero_iff R q p).1 (CharP.cast_eq_zero _ _))

Mathlib/Algebra/GeomSum.lean

@@ -209,9 +209,9 @@ theorem sub_one_dvd_pow_sub_one [Ring α] (x : α) (n : ℕ) :
 
 theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n := by
   cases' le_or_lt y x with h h
-  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
+  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
     exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
-  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
+  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
     exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
 #align nat_sub_dvd_pow_sub_pow nat_sub_dvd_pow_sub_pow
 

Mathlib/Algebra/Group/Hom/Instances.lean

@@ -331,6 +331,14 @@ theorem AddMonoidHom.map_mul_iff (f : R →+ S) :
   Iff.symm AddMonoidHom.ext_iff₂
 #align add_monoid_hom.map_mul_iff AddMonoidHom.map_mul_iff
 
+lemma AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {a : R} :
+    mulLeft a = mulRight a ↔ ∀ b, Commute a b :=
+  FunLike.ext_iff
+
+lemma AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {b : R} :
+    mulRight b = mulLeft b ↔ ∀ a, Commute a b :=
+  FunLike.ext_iff
+
 /-- The left multiplication map: `(a, b) ↦ a * b`. See also `AddMonoidHom.mulLeft`. -/
 @[simps!]
 def AddMonoid.End.mulLeft : R →+ AddMonoid.End R :=
@@ -345,10 +353,6 @@ def AddMonoid.End.mulRight : R →+ AddMonoid.End R :=
 #align add_monoid.End.mul_right AddMonoid.End.mulRight
 #align add_monoid.End.mul_right_apply_apply AddMonoid.End.mulRight_apply_apply
 
-lemma AddMonoid.End.mulRight_eq_mulLeft_of_commute (a : R) (h : ∀ (b : R), Commute a b) :
-    mulRight a = mulLeft a :=
-  AddMonoidHom.ext fun _ ↦ (h _).eq.symm
-
 end Semiring
 
 section CommSemiring
@@ -357,9 +361,9 @@ variable {R S : Type*} [NonUnitalNonAssocCommSemiring R]
 
 namespace AddMonoid.End
 
-lemma comm_mulRight_eq_mulLeft : mulRight = (mulLeft : R →+ AddMonoid.End R) := by
-  ext a
-  exact mulRight_eq_mulLeft_of_commute _ (Commute.all _)
+lemma mulRight_eq_mulLeft : mulRight = (mulLeft : R →+ AddMonoid.End R) :=
+  AddMonoidHom.ext fun _ =>
+    Eq.symm <| AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute.2 (.all _)
 
 end AddMonoid.End