bump to nightly-2023-02-27-03

mathlib commit leanprover-community/mathlib@eb0cb45

Mathbin/Algebra/TrivSqZeroExt.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Eric Wieser
 
 ! This file was ported from Lean 3 source module algebra.triv_sq_zero_ext
-! leanprover-community/mathlib commit b8d2eaa69d69ce8f03179a5cda774fc0cde984e4
+! leanprover-community/mathlib commit eb0cb4511aaef0da2462207b67358a0e1fe1e2ee
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -66,6 +66,8 @@ def TrivSqZeroExt (R : Type u) (M : Type v) :=
 -- mathport name: exprtsze
 local notation "tsze" => TrivSqZeroExt
 
+open BigOperators
+
 namespace TrivSqZeroExt
 
 open MulOpposite (op)
@@ -292,6 +294,16 @@ theorem snd_smul [SMul S R] [SMul S M] (s : S) (x : tsze R M) : (s • x).snd =
   rfl
 #align triv_sq_zero_ext.snd_smul TrivSqZeroExt.snd_smul
 
+theorem fst_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) :
+    (∑ i in s, f i).fst = ∑ i in s, (f i).fst :=
+  Prod.fst_sum
+#align triv_sq_zero_ext.fst_sum TrivSqZeroExt.fst_sum
+
+theorem snd_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) :
+    (∑ i in s, f i).snd = ∑ i in s, (f i).snd :=
+  Prod.snd_sum
+#align triv_sq_zero_ext.snd_sum TrivSqZeroExt.snd_sum
+
 section
 
 variable (M)
@@ -324,6 +336,11 @@ theorem inl_smul [Monoid S] [AddMonoid M] [SMul S R] [DistribMulAction S M] (s :
   ext rfl (smul_zero s).symm
 #align triv_sq_zero_ext.inl_smul TrivSqZeroExt.inl_smul
 
+theorem inl_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → R) :
+    (inl (∑ i in s, f i) : tsze R M) = ∑ i in s, inl (f i) :=
+  (LinearMap.inl ℕ _ _).map_sum
+#align triv_sq_zero_ext.inl_sum TrivSqZeroExt.inl_sum
+
 end
 
 section
@@ -358,6 +375,11 @@ theorem inr_smul [Zero R] [Zero S] [SMulWithZero S R] [SMul S M] (r : S) (m : M)
   ext (smul_zero _).symm rfl
 #align triv_sq_zero_ext.inr_smul TrivSqZeroExt.inr_smul
 
+theorem inr_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
+    (inr (∑ i in s, f i) : tsze R M) = ∑ i in s, inr (f i) :=
+  (LinearMap.inr ℕ _ _).map_sum
+#align triv_sq_zero_ext.inr_sum TrivSqZeroExt.inr_sum
+
 end
 
 theorem inl_fst_add_inr_snd_eq [AddZeroClass R] [AddZeroClass M] (x : tsze R M) :
@@ -558,8 +580,6 @@ instance [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] :
 instance [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] : NonAssocRing (tsze R M) :=
   { TrivSqZeroExt.addGroupWithOne, TrivSqZeroExt.nonAssocSemiring with }
 
-open BigOperators
-
 /-- In the general non-commutative case, the power operator is
 
 $$\begin{align}

Mathbin/All.lean

@@ -1404,6 +1404,7 @@ import Mathbin.Data.Matrix.Basis
 import Mathbin.Data.Matrix.Block
 import Mathbin.Data.Matrix.CharP
 import Mathbin.Data.Matrix.Dmatrix
+import Mathbin.Data.Matrix.DualNumber
 import Mathbin.Data.Matrix.Hadamard
 import Mathbin.Data.Matrix.Kronecker
 import Mathbin.Data.Matrix.Notation
@@ -2240,7 +2241,7 @@ import Mathbin.NumberTheory.Padics.PadicNumbers
 import Mathbin.NumberTheory.Padics.PadicVal
 import Mathbin.NumberTheory.Padics.RingHoms
 import Mathbin.NumberTheory.Pell
-import Mathbin.NumberTheory.PellGeneral
+import Mathbin.NumberTheory.PellMatiyasevic
 import Mathbin.NumberTheory.PrimeCounting
 import Mathbin.NumberTheory.PrimesCongruentOne
 import Mathbin.NumberTheory.Primorial

Mathbin/Data/Finset/Lattice.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.finset.lattice
-! leanprover-community/mathlib commit cc70d9141824ea8982d1562ce009952f2c3ece30
+! leanprover-community/mathlib commit 1c857a1f6798cb054be942199463c2cf904cb937
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -926,7 +926,7 @@ lean 3 declaration is
 but is expected to have type
   forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : DistribLattice.{u2} α] [_inst_2 : OrderBot.{u2} α (Preorder.toLE.{u2} α (PartialOrder.toPreorder.{u2} α (SemilatticeInf.toPartialOrder.{u2} α (Lattice.toSemilatticeInf.{u2} α (DistribLattice.toLattice.{u2} α _inst_1)))))] {s : Finset.{u1} β} {f : β -> α} {a : α}, Iff (Disjoint.{u2} α (SemilatticeInf.toPartialOrder.{u2} α (Lattice.toSemilatticeInf.{u2} α (DistribLattice.toLattice.{u2} α _inst_1))) _inst_2 a (Finset.sup.{u2, u1} α β (Lattice.toSemilatticeSup.{u2} α (DistribLattice.toLattice.{u2} α _inst_1)) _inst_2 s f)) (forall (i : β), (Membership.mem.{u1, u1} β (Finset.{u1} β) (Finset.instMembershipFinset.{u1} β) i s) -> (Disjoint.{u2} α (SemilatticeInf.toPartialOrder.{u2} α (Lattice.toSemilatticeInf.{u2} α (DistribLattice.toLattice.{u2} α _inst_1))) _inst_2 a (f i)))
 Case conversion may be inaccurate. Consider using '#align finset.disjoint_sup_right Finset.disjoint_sup_rightₓ'. -/
-theorem disjoint_sup_right : Disjoint a (s.sup f) ↔ ∀ i ∈ s, Disjoint a (f i) := by
+protected theorem disjoint_sup_right : Disjoint a (s.sup f) ↔ ∀ i ∈ s, Disjoint a (f i) := by
   simp only [disjoint_iff, sup_inf_distrib_left, sup_eq_bot_iff]
 #align finset.disjoint_sup_right Finset.disjoint_sup_right
 
@@ -936,7 +936,7 @@ lean 3 declaration is
 but is expected to have type
   forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : DistribLattice.{u2} α] [_inst_2 : OrderBot.{u2} α (Preorder.toLE.{u2} α (PartialOrder.toPreorder.{u2} α (SemilatticeInf.toPartialOrder.{u2} α (Lattice.toSemilatticeInf.{u2} α (DistribLattice.toLattice.{u2} α _inst_1)))))] {s : Finset.{u1} β} {f : β -> α} {a : α}, Iff (Disjoint.{u2} α (SemilatticeInf.toPartialOrder.{u2} α (Lattice.toSemilatticeInf.{u2} α (DistribLattice.toLattice.{u2} α _inst_1))) _inst_2 (Finset.sup.{u2, u1} α β (Lattice.toSemilatticeSup.{u2} α (DistribLattice.toLattice.{u2} α _inst_1)) _inst_2 s f) a) (forall (i : β), (Membership.mem.{u1, u1} β (Finset.{u1} β) (Finset.instMembershipFinset.{u1} β) i s) -> (Disjoint.{u2} α (SemilatticeInf.toPartialOrder.{u2} α (Lattice.toSemilatticeInf.{u2} α (DistribLattice.toLattice.{u2} α _inst_1))) _inst_2 (f i) a))
 Case conversion may be inaccurate. Consider using '#align finset.disjoint_sup_left Finset.disjoint_sup_leftₓ'. -/
-theorem disjoint_sup_left : Disjoint (s.sup f) a ↔ ∀ i ∈ s, Disjoint (f i) a := by
+protected theorem disjoint_sup_left : Disjoint (s.sup f) a ↔ ∀ i ∈ s, Disjoint (f i) a := by
   simp only [disjoint_iff, sup_inf_distrib_right, sup_eq_bot_iff]
 #align finset.disjoint_sup_left Finset.disjoint_sup_left
 

Mathbin/Data/Matrix/DualNumber.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 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 data.matrix.dual_number
+! leanprover-community/mathlib commit eb0cb4511aaef0da2462207b67358a0e1fe1e2ee
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Algebra.DualNumber
+import Mathbin.Data.Matrix.Basic
+
+/-!
+# Matrices of dual numbers are isomorphic to dual numbers over matrices
+
+Showing this for the more general case of `triv_sq_zero_ext R M` would require an action between
+`matrix n n R` and `matrix n n M`, which would risk causing diamonds.
+-/
+
+
+variable {R n : Type} [CommSemiring R] [Fintype n] [DecidableEq n]
+
+open Matrix TrivSqZeroExt
+
+/-- Matrices over dual numbers and dual numbers over matrices are isomorphic. -/
+@[simps]
+def Matrix.dualNumberEquiv : Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Matrix n n R)
+    where
+  toFun A := ⟨of fun i j => (A i j).fst, of fun i j => (A i j).snd⟩
+  invFun d := of fun i j => (d.fst i j, d.snd i j)
+  left_inv A := Matrix.ext fun i j => TrivSqZeroExt.ext rfl rfl
+  right_inv d := TrivSqZeroExt.ext (Matrix.ext fun i j => rfl) (Matrix.ext fun i j => rfl)
+  map_mul' A B := by
+    ext <;> dsimp [mul_apply]
+    · simp_rw [fst_sum, fst_mul]
+    · simp_rw [snd_sum, snd_mul, smul_eq_mul, op_smul_eq_mul, Finset.sum_add_distrib]
+  map_add' A B := TrivSqZeroExt.ext rfl rfl
+  commutes' r :=
+    by
+    simp_rw [algebra_map_eq_inl', algebra_map_eq_diagonal, Pi.algebraMap_def,
+      Algebra.id.map_eq_self, algebra_map_eq_inl, ← diagonal_map (inl_zero R), map_apply, fst_inl,
+      snd_inl]
+    rfl
+#align matrix.dual_number_equiv Matrix.dualNumberEquiv
+

Mathbin/Data/Polynomial/AlgebraMap.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module data.polynomial.algebra_map
-! leanprover-community/mathlib commit cbdf7b565832144d024caa5a550117c6df0204a5
+! leanprover-community/mathlib commit e064a7bf82ad94c3c17b5128bbd860d1ec34874e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -289,6 +289,12 @@ theorem coe_aeval_eq_eval (r : R) : (aeval r : R[X] → R) = eval r :=
   rfl
 #align polynomial.coe_aeval_eq_eval Polynomial.coe_aeval_eq_eval
 
+@[simp]
+theorem coe_aeval_eq_evalRingHom (x : R) :
+    ((aeval x : R[X] →ₐ[R] R) : R[X] →+* R) = evalRingHom x :=
+  rfl
+#align polynomial.coe_aeval_eq_eval_ring_hom Polynomial.coe_aeval_eq_evalRingHom
+
 @[simp]
 theorem aeval_fn_apply {X : Type _} (g : R[X]) (f : X → R) (x : X) :
     ((aeval f) g) x = aeval (f x) g :=

Mathbin/Data/Polynomial/Div.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, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module data.polynomial.div
-! leanprover-community/mathlib commit 3d32bf9cef95940e3fe1ca0dd2412e0f21579f46
+! leanprover-community/mathlib commit e064a7bf82ad94c3c17b5128bbd860d1ec34874e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathbin.Data.Polynomial.AlgebraMap
 import Mathbin.Data.Polynomial.Inductions
 import Mathbin.Data.Polynomial.Monic
 import Mathbin.RingTheory.Multiplicity
@@ -495,6 +496,34 @@ theorem not_isField : ¬IsField R[X] := by
 
 variable {R}
 
+theorem ker_evalRingHom (x : R) : (evalRingHom x).ker = Ideal.span {x - c x} :=
+  by
+  ext y
+  simpa only [Ideal.mem_span_singleton, dvd_iff_is_root]
+#align polynomial.ker_eval_ring_hom Polynomial.ker_evalRingHom
+
+/-- For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an
+isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$. -/
+noncomputable def quotientSpanXSubCAlgEquiv (x : R) :
+    (R[X] ⧸ Ideal.span ({x - c x} : Set R[X])) ≃ₐ[R] R :=
+  (AlgEquiv.restrictScalars R <|
+          Ideal.quotientEquivAlgOfEq R
+            (ker_eval_ring_hom x : RingHom.ker (aeval x).toRingHom = _)).symm.trans <|
+    Ideal.quotientKerAlgEquivOfRightInverse fun _ => eval_c
+#align polynomial.quotient_span_X_sub_C_alg_equiv Polynomial.quotientSpanXSubCAlgEquiv
+
+@[simp]
+theorem quotientSpanXSubCAlgEquiv_mk (x : R) (p : R[X]) :
+    quotientSpanXSubCAlgEquiv x (Ideal.Quotient.mk _ p) = p.eval x :=
+  rfl
+#align polynomial.quotient_span_X_sub_C_alg_equiv_mk Polynomial.quotientSpanXSubCAlgEquiv_mk
+
+@[simp]
+theorem quotientSpanXSubCAlgEquiv_symm_apply (x : R) (y : R) :
+    (quotientSpanXSubCAlgEquiv x).symm y = algebraMap R _ y :=
+  rfl
+#align polynomial.quotient_span_X_sub_C_alg_equiv_symm_apply Polynomial.quotientSpanXSubCAlgEquiv_symm_apply
+
 section multiplicity
 
 /-- An algorithm for deciding polynomial divisibility.

Mathbin/Data/Polynomial/Eval.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module data.polynomial.eval
-! leanprover-community/mathlib commit 565eb991e264d0db702722b4bde52ee5173c9950
+! leanprover-community/mathlib commit e064a7bf82ad94c3c17b5128bbd860d1ec34874e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -523,6 +523,9 @@ theorem IsRoot.dvd {R : Type _} [CommSemiring R] {p q : R[X]} {x : R} (h : p.IsR
 theorem not_isRoot_c (r a : R) (hr : r ≠ 0) : ¬IsRoot (c r) a := by simpa using hr
 #align polynomial.not_is_root_C Polynomial.not_isRoot_c
 
+theorem eval_surjective (x : R) : Function.Surjective <| eval x := fun y => ⟨c y, eval_c⟩
+#align polynomial.eval_surjective Polynomial.eval_surjective
+
 end Eval
 
 section Comp

Mathbin/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module measure_theory.measure.measure_space_def
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 146a2eed7ad5887ade571e073d0805d2ac618043
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -21,10 +21,10 @@ Given a measurable space `α`, a measure on `α` is a function that sends measur
 extended nonnegative reals that satisfies the following conditions:
 1. `μ ∅ = 0`;
 2. `μ` is countably additive. This means that the measure of a countable union of pairwise disjoint
-   sets is equal to the measure of the individual sets.
+   sets is equal to the sum of the measures of the individual sets.
 
 Every measure can be canonically extended to an outer measure, so that it assigns values to
-all subsets, not just the measurable subsets. On the other hand, a measure that is countably
+all subsets, not just the measurable subsets. On the other hand, an outer measure that is countably
 additive on measurable sets can be restricted to measurable sets to obtain a measure.
 In this file a measure is defined to be an outer measure that is countably additive on
 measurable sets, with the additional assumption that the outer measure is the canonical

Mathbin/NumberTheory/Dioph.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module number_theory.dioph
-! leanprover-community/mathlib commit 356447fe00e75e54777321045cdff7c9ea212e60
+! leanprover-community/mathlib commit a66d07e27d5b5b8ac1147cacfe353478e5c14002
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Data.Fin.Fin2
 import Mathbin.Data.Pfun
 import Mathbin.Data.Vector3
-import Mathbin.NumberTheory.Pell
+import Mathbin.NumberTheory.PellMatiyasevic
 
 /-!
 # Diophantine functions and Matiyasevic's theorem