bump to nightly-2023-05-14-02

mathlib commit leanprover-community/mathlib@e3fb840
leanprover-community · May 14, 2023 · fbb256b · fbb256b
1 parent 44d800a
commit fbb256b
Show file tree

Hide file tree

Showing 36 changed files with 4,288 additions and 3,788 deletions.
diff --git a/Mathbin/Algebra/Homology/ShortExact/Abelian.lean b/Mathbin/Algebra/Homology/ShortExact/Abelian.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Andrew Yang, Pierre-Alexandre Bazin
 
 ! This file was ported from Lean 3 source module algebra.homology.short_exact.abelian
-! leanprover-community/mathlib commit 356447fe00e75e54777321045cdff7c9ea212e60
+! leanprover-community/mathlib commit 6cf5900728239efa287df7761ec2a1ac9cf39b29
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.Abelian.DiagramLemmas.Four
 /-!
 # Short exact sequences in abelian categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In an abelian category, a left-split or right-split short exact sequence admits a splitting.
 -/
 

diff --git a/Mathbin/Algebra/Modeq.lean b/Mathbin/Algebra/Modeq.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module algebra.modeq
-! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c
+! leanprover-community/mathlib commit 6cf5900728239efa287df7761ec2a1ac9cf39b29
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.GroupTheory.QuotientGroup
 /-!
 # Equality modulo an element
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines equality modulo an element in a commutative group.
 
 ## Main definitions

diff --git a/Mathbin/Algebra/Ring/BooleanRing.lean b/Mathbin/Algebra/Ring/BooleanRing.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Yaël Dillies
 
 ! This file was ported from Lean 3 source module algebra.ring.boolean_ring
-! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
+! leanprover-community/mathlib commit 6cf5900728239efa287df7761ec2a1ac9cf39b29
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Order.Hom.Lattice
 /-!
 # Boolean rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A Boolean ring is a ring where multiplication is idempotent. They are equivalent to Boolean
 algebras.
 

diff --git a/Mathbin/All.lean b/Mathbin/All.lean
@@ -518,7 +518,15 @@ import Mathbin.Analysis.Calculus.Deriv
 import Mathbin.Analysis.Calculus.DiffContOnCl
 import Mathbin.Analysis.Calculus.Dslope
 import Mathbin.Analysis.Calculus.ExtendDeriv
-import Mathbin.Analysis.Calculus.Fderiv
+import Mathbin.Analysis.Calculus.Fderiv.Add
+import Mathbin.Analysis.Calculus.Fderiv.Basic
+import Mathbin.Analysis.Calculus.Fderiv.Bilinear
+import Mathbin.Analysis.Calculus.Fderiv.Comp
+import Mathbin.Analysis.Calculus.Fderiv.Equiv
+import Mathbin.Analysis.Calculus.Fderiv.Linear
+import Mathbin.Analysis.Calculus.Fderiv.Mul
+import Mathbin.Analysis.Calculus.Fderiv.Prod
+import Mathbin.Analysis.Calculus.Fderiv.RestrictScalars
 import Mathbin.Analysis.Calculus.FderivAnalytic
 import Mathbin.Analysis.Calculus.FderivMeasurable
 import Mathbin.Analysis.Calculus.FderivSymmetric

diff --git a/Mathbin/Analysis/BoxIntegral/DivergenceTheorem.lean b/Mathbin/Analysis/BoxIntegral/DivergenceTheorem.lean
@@ -4,13 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.box_integral.divergence_theorem
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Analysis.BoxIntegral.Basic
 import Mathbin.Analysis.BoxIntegral.Partition.Additive
-import Mathbin.Analysis.Calculus.Fderiv
+import Mathbin.Analysis.Calculus.Fderiv.Add
+import Mathbin.Analysis.Calculus.Fderiv.Mul
+import Mathbin.Analysis.Calculus.Fderiv.Equiv
+import Mathbin.Analysis.Calculus.Fderiv.RestrictScalars
 
 /-!
 # Divergence integral for Henstock-Kurzweil integral

diff --git a/Mathbin/Analysis/Calculus/Conformal/NormedSpace.lean b/Mathbin/Analysis/Calculus/Conformal/NormedSpace.lean
@@ -4,12 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang
 
 ! This file was ported from Lean 3 source module analysis.calculus.conformal.normed_space
-! leanprover-community/mathlib commit df78eae582aad2f545024bf6c7249191d2723074
+! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Analysis.NormedSpace.ConformalLinearMap
-import Mathbin.Analysis.Calculus.Fderiv
+import Mathbin.Analysis.Calculus.Fderiv.Add
+import Mathbin.Analysis.Calculus.Fderiv.Mul
+import Mathbin.Analysis.Calculus.Fderiv.Equiv
+import Mathbin.Analysis.Calculus.Fderiv.RestrictScalars
 
 /-!
 # Conformal Maps

diff --git a/Mathbin/Analysis/Calculus/ContDiffDef.lean b/Mathbin/Analysis/Calculus/ContDiffDef.lean
@@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module analysis.calculus.cont_diff_def
-! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1
+! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Analysis.Calculus.Fderiv
+import Mathbin.Analysis.Calculus.Fderiv.Add
+import Mathbin.Analysis.Calculus.Fderiv.Mul
+import Mathbin.Analysis.Calculus.Fderiv.Equiv
+import Mathbin.Analysis.Calculus.Fderiv.RestrictScalars
 import Mathbin.Analysis.Calculus.FormalMultilinearSeries
 
 /-!

diff --git a/Mathbin/Analysis/Calculus/Deriv.lean b/Mathbin/Analysis/Calculus/Deriv.lean
@@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module analysis.calculus.deriv
-! leanprover-community/mathlib commit f81174bd8aa3896304e8e1c1cb1d11cb0e0a05df
+! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Analysis.Calculus.Fderiv
+import Mathbin.Analysis.Calculus.Fderiv.Add
+import Mathbin.Analysis.Calculus.Fderiv.Mul
+import Mathbin.Analysis.Calculus.Fderiv.Equiv
+import Mathbin.Analysis.Calculus.Fderiv.RestrictScalars
 import Mathbin.Data.Polynomial.AlgebraMap
 import Mathbin.Data.Polynomial.Derivative
 import Mathbin.LinearAlgebra.AffineSpace.Slope