bump to nightly-2023-06-06-03

mathlib commit leanprover-community/mathlib@a3209dd
leanprover-community · Jun 6, 2023 · 90f9e14 · 90f9e14
1 parent b72456a
commit 90f9e14
Show file tree

Hide file tree

Showing 37 changed files with 2,231 additions and 1,517 deletions.
diff --git a/Mathbin/Algebra/Lie/TensorProduct.lean b/Mathbin/Algebra/Lie/TensorProduct.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.tensor_product
-! leanprover-community/mathlib commit 657df4339ae6ceada048c8a2980fb10e393143ec
+! leanprover-community/mathlib commit 575b4ea3738b017e30fb205cb9b4a8742e5e82b6
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Algebra.Lie.Abelian
 /-!
 # Tensor products of Lie modules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Tensor products of Lie modules carry natural Lie module structures.
 
 ## Tags

diff --git a/Mathbin/AlgebraicGeometry/AffineScheme.lean b/Mathbin/AlgebraicGeometry/AffineScheme.lean
@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.AffineScheme
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 533f62f4dd62a5aad24a04326e6e787c8f7e98b1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.AlgebraicGeometry.GammaSpecAdjunction
-import Mathbin.AlgebraicGeometry.OpenImmersion
+import Mathbin.AlgebraicGeometry.OpenImmersion.Scheme
 import Mathbin.CategoryTheory.Limits.Opposites
 import Mathbin.RingTheory.Localization.InvSubmonoid
 

diff --git a/Mathbin/AlgebraicGeometry/Gluing.lean b/Mathbin/AlgebraicGeometry/Gluing.lean
@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.gluing
-! leanprover-community/mathlib commit a9402e0a11843994283cd0a918e61fa51360e26a
+! leanprover-community/mathlib commit 533f62f4dd62a5aad24a04326e6e787c8f7e98b1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.AlgebraicGeometry.PresheafedSpace.Gluing
+import Mathbin.AlgebraicGeometry.OpenImmersion.Scheme
 
 /-!
 # Gluing Schemes

diff --git a/Mathbin/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean b/Mathbin/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean
@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.locally_ringed_space.has_colimits
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 533f62f4dd62a5aad24a04326e6e787c8f7e98b1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.AlgebraicGeometry.LocallyRingedSpace
 import Mathbin.Algebra.Category.Ring.Constructions
-import Mathbin.AlgebraicGeometry.OpenImmersion
+import Mathbin.AlgebraicGeometry.OpenImmersion.Basic
 import Mathbin.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 
 /-!