bump

FltRegular/CaseII/Statement.lean

@@ -12,7 +12,7 @@ variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 namespace FltRegular
 
 include hp hreg in
-lemma not_exists_solution (hm : 1 ≤ m) :
+lemma not_exists_solution {m : ℕ} (hm : 1 ≤ m) :
   ¬∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ),
     ¬((hζ.unit' : 𝓞 K) - 1 ∣ y') ∧ ¬((hζ.unit' : 𝓞 K) - 1 ∣ z') ∧
     x' ^ (p : ℕ) + y' ^ (p : ℕ) = ε₃ * (((hζ.unit' : 𝓞 K) - 1) ^ m * z') ^ (p : ℕ) := by

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -38,7 +38,8 @@ lemma associated_zeta_sub_one_pow_prime : Associated ((hζ.unit' - 1 : 𝓞 K) ^
     ((isPrimitiveRoot_of_mem_primitiveRoots hη).mem_nthRootsFinset hpri.out.pos)
       ((isPrimitiveRoot_of_mem_primitiveRoots hη).ne_one hpri.out.one_lt).symm
 
-lemma isCoprime_of_not_zeta_sub_one_dvd (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x) : IsCoprime ↑p x := by
+lemma isCoprime_of_not_zeta_sub_one_dvd {x : 𝓞 K} (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x) :
+    IsCoprime ↑p x := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   rwa [← Ideal.isCoprime_span_singleton_iff,
     ← Ideal.span_singleton_eq_span_singleton.mpr (associated_zeta_sub_one_pow_prime hζ),

FltRegular/NumberTheory/Finrank.lean

@@ -6,35 +6,26 @@ import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.Dimension.Localization
 
 open Module
-
 section
 
-universe u v
-
-variable (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M]
-
-variable {R M}
-
-variable [StrongRankCondition R] [Module.Finite R M]
+variable (R M : Type*) [Ring R] [AddCommGroup M] [Module R M]
 
-instance torsion.module {R M} [Ring R] [AddCommGroup M] [Module R M] :
-    Module R (M ⧸ AddCommGroup.torsion M) := by
+instance torsion.module : Module R (M ⧸ AddCommGroup.torsion M) := by
   letI : Submodule R M := { AddCommGroup.torsion M with smul_mem' := fun r m ⟨n, hn, hn'⟩ ↦
     ⟨n, hn, by { simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
       Nat.isUnit_iff, smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }⟩ }
   exact inferInstanceAs (Module R (M ⧸ this))
 
 end
 
-variable {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M]
-variable [Module R M] (N : Submodule R M)
+variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M)
 
 lemma FiniteDimensional.finrank_quotient_of_le_torsion (hN : N ≤ Submodule.torsion R M) :
     finrank R (M ⧸ N) = finrank R M := congr_arg Cardinal.toNat (rank_quotient_eq_of_le_torsion hN)
 
-lemma FiniteDimensional.finrank_map_of_le_torsion {M'} [AddCommGroup M'] [Module R M']
-    (l : M →ₗ[R] M') [Module.Finite R N]
-    (hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M) : finrank R (N.map l) = finrank R N := by
+lemma FiniteDimensional.finrank_map_of_le_torsion {M' : Type*} [AddCommGroup M'] [Module R M']
+    (l : M →ₗ[R] M') [Module.Finite R N] (hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M) :
+      finrank R (N.map l) = finrank R N := by
   conv_lhs => rw [← N.range_subtype, ← LinearMap.range_comp,
     ← (LinearMap.quotKerEquivRange (l.comp N.subtype)).finrank_eq]
   apply FiniteDimensional.finrank_quotient_of_le_torsion
@@ -68,7 +59,7 @@ instance [IsDomain R] [IsPrincipalIdealRing R] : Module.Free R (M ⧸ Submodule.
 
 lemma FiniteDimensional.finrank_add_finrank_quotient [IsDomain R] (N : Submodule R M) :
     finrank R (M ⧸ N) + finrank R N = finrank R M := by
-  rw [← Cardinal.natCast_inj.{v}, Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
+  rw [← Cardinal.natCast_inj, Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
     Submodule.finrank_eq_rank]
   exact HasRankNullity.rank_quotient_add_rank _
 

FltRegular/NumberTheory/Hilbert92.lean

@@ -11,7 +11,7 @@ import Mathlib.RingTheory.Henselian
 open scoped NumberField nonZeroDivisors
 open FiniteDimensional NumberField
 
-variable (p : ℕ+) {K : Type*} [Field K]
+variable {s r : ℕ} (p : ℕ+) {K : Type*} [Field K]
 variable {k : Type*} [Field k] (hp : Nat.Prime p)
 
 open Module BigOperators Finset
@@ -23,12 +23,12 @@ variable (G : Type*) [AddCommGroup G]
 local notation3 "A" => CyclotomicIntegers p
 
 /-The system of units is maximal if the quotient by its span leaves a torsion module (i.e. finite) -/
-abbrev systemOfUnits.IsMaximal {s : ℕ} {p : ℕ+} {G : Type*} [AddCommGroup G]
+abbrev systemOfUnits.IsMaximal {p : ℕ+} {G : Type*} [AddCommGroup G]
     [Module (CyclotomicIntegers p) G] (sys : systemOfUnits (G := G) p s) :=
   Fintype (G ⧸ Submodule.span (CyclotomicIntegers p) (Set.range sys.units))
 
 noncomputable
-def systemOfUnits.isMaximal [Module.Finite ℤ G] {s : ℕ} (hf : finrank ℤ G = s * (p - 1))
+def systemOfUnits.isMaximal [Module.Finite ℤ G] (hf : finrank ℤ G = s * (p - 1))
   [Module A G] (sys : systemOfUnits (G := G) p s) : sys.IsMaximal := by
   apply Nonempty.some
   apply (@nonempty_fintype _ ?_)

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dd6b1019b5cef990161bf3edfebeb6b0be78044a",
+   "rev": "7c5548eeeb1748da5c2872dbd866d3acbaea4b3f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,12 +75,22 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d43bc00b660d5456721455c8f4e4d1d2244f555b",
+   "rev": "970a6567fb2a41652d0ef34ee38c464dc2b76233",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,

lakefile.lean

@@ -1,17 +1,41 @@
 import Lake
 open Lake DSL
 
-package «flt-regular» {
-  -- add any package configuration options here
-}
+def moreServerArgs := #[
+  "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
+  "-DautoImplicit=false",
+  "-DrelaxedAutoImplicit=false"
+]
+
+-- These settings only apply during `lake build`, but not in VSCode editor.
+def moreLeanArgs := moreServerArgs
+
+-- These are additional settings which do not affect the lake hash,
+-- so they can be enabled in CI and disabled locally or vice versa.
+-- Warning: Do not put any options here that actually change the olean files,
+-- or inconsistent behavior may result
+def weakLeanArgs : Array String :=
+  if get_config? CI |>.isSome then
+    #["-DwarningAsError=true"]
+  else
+    #[]
+
+package «flt-regular» where
+  leanOptions := #[
+    ⟨`relaxedAutoImplicit, false⟩, -- prevents typos to be interpreted as new free variables
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`autoImplicit, false⟩]
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
+require checkdecls from git
+  "https://github.com/PatrickMassot/checkdecls.git" @ "master"
+
 require «doc-gen4» from git
   "https://github.com/leanprover/doc-gen4" @ "main"
 
 @[default_target]
-lean_lib «FltRegular» {
-  -- add any library configuration options here
-}
+lean_lib «FltRegular» where
+  moreLeanArgs := moreLeanArgs
+  weakLeanArgs := weakLeanArgs