From c99e6bc6c8f261f96e16f7f1bc26a6f0125e8959 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 12 Jan 2025 18:44:43 +0000 Subject: [PATCH] Update Mathlib/Topology/Algebra/Module/ModuleTopology.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Topology/Algebra/Module/ModuleTopology.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/Mathlib/Topology/Algebra/Module/ModuleTopology.lean index 2d8c514091988..d93e0243f2c58 100644 --- a/Mathlib/Topology/Algebra/Module/ModuleTopology.lean +++ b/Mathlib/Topology/Algebra/Module/ModuleTopology.lean @@ -433,9 +433,9 @@ instance instProd : IsModuleTopology R (M × N) := by refine le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩ -- Or equivalently, if `P` denotes `M × N` with the module topology, let P := M × N - letI τP : TopologicalSpace P := moduleTopology R P - haveI : IsModuleTopology R P := ⟨rfl⟩ - haveI : ContinuousAdd P := ModuleTopology.continuousAdd R P + let τP : TopologicalSpace P := moduleTopology R P + have : IsModuleTopology R P := ⟨rfl⟩ + have : ContinuousAdd P := ModuleTopology.continuousAdd R P -- and if `i` denotes the identity map from `M × N` to `P` let i : M × N → P := id -- then we need to show that `i` is continuous.