Merge pull request #122 from pitmonticone/fix-FGModuleTopology

Fix `FGModuleTopology`

Author: kbuzzard

FLT/AutomorphicRepresentation/Example.lean

@@ -878,7 +878,7 @@ lemma left_ideal_princ (I : Submodule 𝓞 𝓞) : ∃ a : 𝓞, I = Submodule.s
     rintro _ ⟨_, rfl⟩
     exact norm_nonneg _
   obtain ⟨a, ha⟩ : ∃ a : S, norm a = ⨅ i : S, norm i :=
-    exists_eq_ciInf_of_not_isPredLimit hbdd (Order.not_isPredLimit)
+    exists_eq_ciInf_of_not_isPredPrelimit hbdd (Order.not_isPredPrelimit)
   use a
   apply le_antisymm
   · intro i hi

FLT/ForMathlib/FGModuleTopology.lean

@@ -1,7 +1,7 @@
-import Mathlib.Algebra.Module.Projective
+import FLT.ForMathlib.MiscLemmas
+import Mathlib.Data.Finite.Card
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.Topology.Algebra.Module.Basic
-import FLT.ForMathlib.MiscLemmas
 /-!
 
 # The module topology
@@ -31,8 +31,6 @@ or $p$-adics).
 
 -/
 
-set_option lang.lemmaCmd true
-
 section basics
 
 variable (R : Type*) [TopologicalSpace R] [Semiring R]

lake-manifest.json

@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "df80b0dd2548c76fbdc3fe5d3a96873dfd46c0dc",
+   "rev": "3fecb249afcf5ba40efe0a3f92f69e2460f142c7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,