please stop

FltRegular/NumberTheory/Hilbert92.lean

@@ -23,27 +23,27 @@ 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 {r} {p : ℕ+} {G} [AddCommGroup G] [Module (CyclotomicIntegers p) G]
-    (sys : systemOfUnits (G := G) p r) :=
+abbrev systemOfUnits.IsMaximal {s : ℕ} {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] {r} (hf : finrank ℤ G = r * (p - 1)) [Module A G]
-  (sys : systemOfUnits (G := G) p r) : sys.IsMaximal := by
+def systemOfUnits.isMaximal [Module.Finite ℤ G] {s : ℕ} (hf : finrank ℤ G = s * (p - 1))
+  [Module A G] (sys : systemOfUnits (G := G) p s) : sys.IsMaximal := by
   apply Nonempty.some
   apply (@nonempty_fintype _ ?_)
   apply Module.finite_of_fg_torsion
   rw [← FiniteDimensional.finrank_eq_zero_iff_isTorsion,  finrank_quotient',
     finrank_spanA p hp _ _ sys.linearIndependent, hf, mul_comm, Nat.sub_self]
 
 noncomputable
-def systemOfUnits.index [Module A G] (sys : systemOfUnits p G r) [sys.IsMaximal] :=
+def systemOfUnits.index [Module A G] (sys : systemOfUnits p G s) [sys.IsMaximal] :=
   Fintype.card (G ⧸ Submodule.span A (Set.range sys.units))
 
 /-- A system of units is fundamental if it's maximal and the submodule generated by the elements
 of the system has smallest index. -/
-def systemOfUnits.IsFundamental [Module A G] (h : systemOfUnits p G r) :=
-  ∃ _ : h.IsMaximal, ∀ (s : systemOfUnits p G r) (_ : s.IsMaximal), h.index ≤ s.index
+def systemOfUnits.IsFundamental [Module A G] (h : systemOfUnits p G s) :=
+  ∃ _ : h.IsMaximal, ∀ (S : systemOfUnits p G s) (_ : S.IsMaximal), h.index ≤ S.index
 
 lemma systemOfUnits.IsFundamental.maximal' [Module A G] (S : systemOfUnits p G r)
     (hs : S.IsFundamental) (a : systemOfUnits p G r) [a.IsMaximal] :
@@ -142,19 +142,19 @@ lemma Subgroup.index_mono {G : Type*} [Group G] {H₁ H₂ : Subgroup G} (h : H
 namespace systemOfUnits.IsFundamental
 
 variable {H : Type*} [CommGroup H] [Fintype H]
-  (hCard : Fintype.card H = p) (σ : H) (hσ : Subgroup.zpowers σ = ⊤) (r : ℕ) [DistribMulAction H G]
-  (hf : finrank ℤ G = r * (p - 1))
+  (hCard : Fintype.card H = p) (σ : H) (hσ : Subgroup.zpowers σ = ⊤) (s : ℕ) [DistribMulAction H G]
+  (hf : finrank ℤ G = s * (p - 1))
 
 include hp hf
 
 variable [Module.Finite ℤ G]
 
 /-there exists an fundamental set of units.-/
 lemma existence [Module.Free ℤ G] [Module A G] :
-    ∃ S : systemOfUnits p G r, S.IsFundamental := by
-  obtain ⟨S⟩ := systemOfUnits.existence p hp G r hf
+    ∃ S : systemOfUnits p G s, S.IsFundamental := by
+  obtain ⟨S⟩ := systemOfUnits.existence p hp G s hf
   letI := S.isMaximal hp hf
-  have : { a | ∃ (S : systemOfUnits p G r) (_ : S.IsMaximal), a = S.index p G }.Nonempty :=
+  have : { a | ∃ (S : systemOfUnits p G s) (_ : S.IsMaximal), a = S.index p G }.Nonempty :=
     ⟨S.index, S, S.isMaximal hp hf, rfl⟩
   obtain ⟨S', hS', ha⟩ := Nat.sInf_mem this
   use S', hS'
@@ -163,14 +163,14 @@ lemma existence [Module.Free ℤ G] [Module A G] :
   apply csInf_le (OrderBot.bddBelow _)
   use a', ha'
 
-lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental)
-    (i : Fin r) (a : Fin r →₀ A) (ha : a i = 1) :
+lemma lemma2 [Module A G] (S : systemOfUnits p G s) (hs : S.IsFundamental)
+    (i : Fin s) (a : Fin s →₀ A) (ha : a i = 1) :
     ∀ g : G, (1 - zeta p) • g ≠ Finsupp.linearCombination A S.units a := by
-  cases' r with r
+  cases' s with s
   · exact isEmptyElim i
   intro g hg
   letI := Fact.mk hp
-  let S' : systemOfUnits p G (r + 1) := ⟨Function.update S.units i g,
+  let S' : systemOfUnits p G (s + 1) := ⟨Function.update S.units i g,
     LinearIndependent.update' _ _ _ _ _ _ (CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors p)
     hg (ha ▸ one_mem A⁰) S.linearIndependent⟩
   let a' := a.comapDomain (Fin.succAbove i) Fin.succAbove_right_injective.injOn
@@ -211,7 +211,7 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental)
     rintro ⟨l, rfl⟩
     letI := (Algebra.id A).toModule
     letI : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
-    letI : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
+    letI : Module A (Fin s →₀ A) := Finsupp.module (Fin s) A
     rw [← LinearMap.map_smul, ← sub_eq_zero,
       ← (Finsupp.linearCombination A S.units).map_sub] at hg
     have := DFunLike.congr_fun (linearIndependent_iff.mp S.linearIndependent _ hg) i
@@ -220,17 +220,17 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental)
     exact CyclotomicIntegers.not_isUnit_one_sub_zeta p
       (isUnit_of_mul_eq_one _ _ this)
 
-lemma corollary [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (a : Fin r → ℤ)
+lemma corollary [Module A G] (S : systemOfUnits p G s) (hs : S.IsFundamental) (a : Fin s → ℤ)
     (ha : ∃ i , ¬ (p : ℤ) ∣ a i) :
     ∀ g : G, (1 - zeta p) • g ≠ ∑ i, a i • S.units i := by
   intro g hg
   obtain ⟨i, hi⟩ := ha
   letI := Fact.mk hp
   obtain ⟨x, y, e⟩ := CyclotomicIntegers.isCoprime_one_sub_zeta p (a i) hi
-  let b' : Fin r → A := fun j ↦ x * (1 - zeta ↑p) + y * (a j)
+  let b' : Fin s → A := fun j ↦ x * (1 - zeta ↑p) + y * (a j)
   let b := Finsupp.ofSupportFinite b' (Set.toFinite (Function.support _))
   have hb : b i = 1 := by rw [← e]; rfl
-  apply lemma2 p hp G r hf S hs i b hb (x • ∑ i, S.units i + y • g)
+  apply lemma2 p hp G s hf S hs i b hb (x • ∑ i, S.units i + y • g)
   rw [smul_add, smul_smul _ y, mul_comm, ← smul_smul, hg, smul_sum, smul_sum, smul_sum,
     ← sum_add_distrib, Finsupp.linearCombination_apply, Finsupp.sum_fintype]
   congr