bump to nightly-2023-07-28-03

mathlib commit leanprover-community/mathlib@fe18ded

Archive/All.lean

@@ -53,5 +53,5 @@ import Archive.Wiedijk100Theorems.PerfectNumbers
 import Archive.Wiedijk100Theorems.SolutionOfCubic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 
-#align_import all from "leanprover-community/mathlib"@"d11f435d4e34a6cea0a1797d6b625b0c170be845"
+#align_import all from "leanprover-community/mathlib"@"fe18deda804e30c594e75a6e5fe0f7d14695289f"
 

Counterexamples/All.lean

@@ -13,5 +13,5 @@ import Counterexamples.SeminormLatticeNotDistrib
 import Counterexamples.SorgenfreyLine
 import Counterexamples.ZeroDivisorsInAddMonoidAlgebras
 
-#align_import all from "leanprover-community/mathlib"@"d11f435d4e34a6cea0a1797d6b625b0c170be845"
+#align_import all from "leanprover-community/mathlib"@"fe18deda804e30c594e75a6e5fe0f7d14695289f"
 

Mathbin/All.lean

@@ -3213,5 +3213,5 @@ import Mathbin.Topology.VectorBundle.Basic
 import Mathbin.Topology.VectorBundle.Constructions
 import Mathbin.Topology.VectorBundle.Hom
 
-#align_import all from "leanprover-community/mathlib"@"d11f435d4e34a6cea0a1797d6b625b0c170be845"
+#align_import all from "leanprover-community/mathlib"@"fe18deda804e30c594e75a6e5fe0f7d14695289f"
 

Mathbin/Analysis/NormedSpace/ContinuousLinearMap.lean

@@ -5,7 +5,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 -/
 import Mathbin.Analysis.NormedSpace.Basic
 
-#align_import analysis.normed_space.continuous_linear_map from "leanprover-community/mathlib"@"41bef4ae1254365bc190aee63b947674d2977f01"
+#align_import analysis.normed_space.continuous_linear_map from "leanprover-community/mathlib"@"fe18deda804e30c594e75a6e5fe0f7d14695289f"
 
 /-! # Constructions of continuous linear maps between (semi-)normed spaces
 
@@ -39,16 +39,16 @@ open scoped NNReal
 
 variable {𝕜 𝕜₂ E F G : Type _}
 
-variable [NormedField 𝕜] [NormedField 𝕜₂]
-
 /-! # General constructions -/
 
 
-section Seminormed
+section SeminormedAddCommGroup
+
+variable [Ring 𝕜] [Ring 𝕜₂]
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G]
 
-variable [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 G]
+variable [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 G]
 
 variable {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F)
 
@@ -61,16 +61,6 @@ def LinearMap.mkContinuous (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : E
 #align linear_map.mk_continuous LinearMap.mkContinuous
 -/
 
-#print LinearMap.toContinuousLinearMap₁ /-
-/-- Reinterpret a linear map `𝕜 →ₗ[𝕜] E` as a continuous linear map. This construction
-is generalized to the case of any finite dimensional domain
-in `linear_map.to_continuous_linear_map`. -/
-def LinearMap.toContinuousLinearMap₁ (f : 𝕜 →ₗ[𝕜] E) : 𝕜 →L[𝕜] E :=
-  f.mkContinuous ‖f 1‖ fun x =>
-    le_of_eq <| by conv_lhs => rw [← mul_one x]; rw [← smul_eq_mul, f.map_smul, norm_smul, mul_comm]
-#align linear_map.to_continuous_linear_map₁ LinearMap.toContinuousLinearMap₁
--/
-
 #print LinearMap.mkContinuousOfExistsBound /-
 /-- Construct a continuous linear map from a linear map and the existence of a bound on this linear
 map. If you have an explicit bound, use `linear_map.mk_continuous` instead, as a norm estimate will
@@ -138,22 +128,6 @@ theorem LinearMap.mkContinuousOfExistsBound_apply (h : ∃ C, ∀ x, ‖f x‖ 
 #align linear_map.mk_continuous_of_exists_bound_apply LinearMap.mkContinuousOfExistsBound_apply
 -/
 
-#print LinearMap.toContinuousLinearMap₁_coe /-
-@[simp]
-theorem LinearMap.toContinuousLinearMap₁_coe (f : 𝕜 →ₗ[𝕜] E) :
-    (f.toContinuousLinearMap₁ : 𝕜 →ₗ[𝕜] E) = f :=
-  rfl
-#align linear_map.to_continuous_linear_map₁_coe LinearMap.toContinuousLinearMap₁_coe
--/
-
-#print LinearMap.toContinuousLinearMap₁_apply /-
-@[simp]
-theorem LinearMap.toContinuousLinearMap₁_apply (f : 𝕜 →ₗ[𝕜] E) (x) :
-    f.toContinuousLinearMap₁ x = f x :=
-  rfl
-#align linear_map.to_continuous_linear_map₁_apply LinearMap.toContinuousLinearMap₁_apply
--/
-
 namespace ContinuousLinearMap
 
 #print ContinuousLinearMap.antilipschitz_of_bound /-
@@ -190,11 +164,47 @@ def LinearEquiv.toContinuousLinearEquivOfBounds (e : E ≃ₛₗ[σ] F) (C_to C_
 
 end
 
-end Seminormed
+end SeminormedAddCommGroup
+
+section SeminormedBounded
+
+variable [SeminormedRing 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E]
+
+variable [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
+#print LinearMap.toContinuousLinearMap₁ /-
+/-- Reinterpret a linear map `𝕜 →ₗ[𝕜] E` as a continuous linear map. This construction
+is generalized to the case of any finite dimensional domain
+in `linear_map.to_continuous_linear_map`. -/
+def LinearMap.toContinuousLinearMap₁ (f : 𝕜 →ₗ[𝕜] E) : 𝕜 →L[𝕜] E :=
+  f.mkContinuous ‖f 1‖ fun x => by conv_lhs => rw [← mul_one x];
+    rw [← smul_eq_mul, f.map_smul, mul_comm]; exact norm_smul_le _ _
+#align linear_map.to_continuous_linear_map₁ LinearMap.toContinuousLinearMap₁
+-/
+
+#print LinearMap.toContinuousLinearMap₁_coe /-
+@[simp]
+theorem LinearMap.toContinuousLinearMap₁_coe (f : 𝕜 →ₗ[𝕜] E) :
+    (f.toContinuousLinearMap₁ : 𝕜 →ₗ[𝕜] E) = f :=
+  rfl
+#align linear_map.to_continuous_linear_map₁_coe LinearMap.toContinuousLinearMap₁_coe
+-/
+
+#print LinearMap.toContinuousLinearMap₁_apply /-
+@[simp]
+theorem LinearMap.toContinuousLinearMap₁_apply (f : 𝕜 →ₗ[𝕜] E) (x) :
+    f.toContinuousLinearMap₁ x = f x :=
+  rfl
+#align linear_map.to_continuous_linear_map₁_apply LinearMap.toContinuousLinearMap₁_apply
+-/
+
+end SeminormedBounded
 
 section Normed
 
-variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F]
+variable [Ring 𝕜] [Ring 𝕜₂]
+
+variable [NormedAddCommGroup E] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F]
 
 variable {σ : 𝕜 →+* 𝕜₂} (f g : E →SL[σ] F) (x y z : E)
 
@@ -212,9 +222,11 @@ end Normed
 
 section Seminormed
 
+variable [Ring 𝕜] [Ring 𝕜₂]
+
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F]
 
-variable [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F]
+variable [Module 𝕜 E] [Module 𝕜₂ F]
 
 variable {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F)
 
@@ -259,48 +271,44 @@ end Seminormed
 /-! ## The span of a single vector -/
 
 
-section Seminormed
-
-variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-
 namespace ContinuousLinearMap
 
 variable (𝕜)
 
+section Seminormed
+
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
 #print ContinuousLinearMap.toSpanSingleton_homothety /-
 theorem toSpanSingleton_homothety (x : E) (c : 𝕜) :
     ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ := by rw [mul_comm]; exact norm_smul _ _
 #align continuous_linear_map.to_span_singleton_homothety ContinuousLinearMap.toSpanSingleton_homothety
 -/
 
-end ContinuousLinearMap
+end Seminormed
 
-section
+end ContinuousLinearMap
 
 namespace ContinuousLinearEquiv
 
 variable (𝕜)
 
+section Seminormed
+
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
 #print ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety /-
 theorem toSpanNonzeroSingleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
     ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖ :=
   ContinuousLinearMap.toSpanSingleton_homothety _ _ _
 #align continuous_linear_equiv.to_span_nonzero_singleton_homothety ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety
 -/
 
-end ContinuousLinearEquiv
-
-end
-
 end Seminormed
 
 section Normed
 
-variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-
-namespace ContinuousLinearEquiv
-
-variable (𝕜)
+variable [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 #print ContinuousLinearEquiv.toSpanNonzeroSingleton /-
 /-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
@@ -351,7 +359,7 @@ theorem coord_self (x : E) (h : x ≠ 0) :
 #align continuous_linear_equiv.coord_self ContinuousLinearEquiv.coord_self
 -/
 
-end ContinuousLinearEquiv
-
 end Normed
 
+end ContinuousLinearEquiv
+

README.md

@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`d11f435d4e34a6cea0a1797d6b625b0c170be845`](https://github.com/leanprover-community/mathlib/commit/d11f435d4e34a6cea0a1797d6b625b0c170be845)
+Tracking mathlib commit: [`fe18deda804e30c594e75a6e5fe0f7d14695289f`](https://github.com/leanprover-community/mathlib/commit/fe18deda804e30c594e75a6e5fe0f7d14695289f)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "61d54fcf7b6afabc5b4fdc5867b261eb5ddd5fc4",
+    "rev": "cded5c37f591ab1fce76c1fb571b81e36766e48a",
     "name": "lean3port",
-    "inputRev?": "61d54fcf7b6afabc5b4fdc5867b261eb5ddd5fc4"}},
+    "inputRev?": "cded5c37f591ab1fce76c1fb571b81e36766e48a"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-07-28-01"
+def tag : String := "nightly-2023-07-28-03"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"61d54fcf7b6afabc5b4fdc5867b261eb5ddd5fc4"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"cded5c37f591ab1fce76c1fb571b81e36766e48a"
 
 @[default_target]
 lean_lib Mathbin where

upstream-rev

@@ -1 +1 @@
-d11f435d4e34a6cea0a1797d6b625b0c170be845
+fe18deda804e30c594e75a6e5fe0f7d14695289f