bump

.vscode/settings.json

@@ -1,4 +1,28 @@
 {
+"files.exclude": {
+        "**/.git": true,
+        "**/.DS_Store": true,
+        "**/*.olean": true,
+        "**/.DS_yml": true,
+        "**/.gitpod.yml": true,
+        "**/.vscode": true,
+	".docker": true,
+	"build": true,
+	"html": true,
+	"lake-packages": true,
+	".gitignore": true,
+	"lake-manifest.json": true,
+	"lakefile.lean": true,
+	"README.md": true,
+	"Library.lean": true,
+	"lean-toolchain": true,
+	"img": true,
+	".lake": true,
+	".github": true,
+    "LICENSE":true,
+    ".devcontainer":true,
+    "lean-tactics.tex":true,
+    },
     "editor.insertSpaces": true,
     "editor.tabSize": 2,
     "editor.rulers" : [100],

FltRegular/CaseI/AuxLemmas.lean

@@ -59,7 +59,7 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   rw [show (k₁ : ℤ) = 0 by simpa using habs, zero_sub] at hcong
   rw [habs, _root_.pow_zero, mul_one, add_sub_cancel_left, aux_cong0k₁ hpri hcong] at hdiv
   nth_rw 1 [show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
-  have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by
+  have key : ↑(p : ℤ) ∣ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j := by
     convert hdiv using 1
     have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm]
     simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h,
@@ -107,7 +107,7 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ
     Int.cast_zero, sub_eq_zero, ZMod.intCast_eq_intCast_iff] at hcong
   rw [habs, _root_.pow_zero, mul_one, aux_cong0k₂ hpri hcong, Fin.val_mk, pow_one, add_sub_assoc,
     ← sub_mul, add_sub_right_comm, show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
-  have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₂ a b j • ζ ^ j := by
+  have key : ↑(p : ℤ) ∣ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j := by
     convert hdiv using 1
     simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one,
       Finset.range_filter_eq]
@@ -182,8 +182,8 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
     sub_eq_iff_eq_add, ← Int.cast_add, ZMod.intCast_eq_intCast_iff] at hcong
   rw [habs, pow_one, aux_cong1k₂ hpri hp5 hcong] at hdiv
   ring_nf at hdiv
-  have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by
-    suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
+  have key : ↑(p : ℤ) ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j := by
+    suffices ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
       rwa [this]
     simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
       (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]

FltRegular/CaseI/Statement.lean

@@ -232,7 +232,7 @@ theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
   have hζ := zeta_spec P ℤ R
   intro H
   obtain ⟨k₁, k₂, hcong, hdiv⟩ := ex_fin_div hp5 hreg hζ hgcd caseI H
-  have key : ↑(p : ℤ) ∣ ∑ j in range p, f a b k₁ k₂ j • ζ ^ j := by
+  have key : ↑(p : ℤ) ∣ ∑ j ∈ range p, f a b k₁ k₂ j • ζ ^ j := by
     convert hdiv using 1
     have h01 : 0 ≠ 1 := zero_ne_one
     have h0k₁ := aux0k₁ hpri.out hp5 hζ caseI hcong hdiv

FltRegular/CaseII/InductionStep.lean

@@ -88,7 +88,7 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   letI : Fact (Nat.Prime p) := hpri
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   have h := zeta_sub_one_dvd hζ e
-  replace h : ∏ _η in nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0 := by
+  replace h : ∏ _η ∈ nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0 := by
     rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <|
       hpri.out.eq_two_or_odd.resolve_left
       (PNat.coe_injective.ne hp), ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h
@@ -247,7 +247,7 @@ lemma exists_ideal_pow_eq_c_aux :
     add_mul, one_mul, pow_add, mul_assoc, mul_assoc, mul_assoc]
 
 /- The ∏_η,  𝔠 η = (𝔷' 𝔭^m)^p with 𝔷 = 𝔪 𝔷' -/
-lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (𝔷' * 𝔭 ^ m) ^ (p : ℕ) := by
+lemma prod_c : ∏ η ∈ Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (𝔷' * 𝔭 ^ m) ^ (p : ℕ) := by
   have e' := span_pow_add_pow_eq hζ e
   rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <|
     hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)] at e'
@@ -314,7 +314,7 @@ lemma p_dvd_c_iff : 𝔭 ∣ (𝔠 η) ↔ η = η₀ := by
 
 /- All the others 𝔠 η are coprime to 𝔭...basically-/
 lemma p_pow_dvd_c_eta_zero_aux [DecidableEq (𝓞 K)] :
-  gcd (𝔭 ^ (m * p)) (∏ η in Finset.attach (nthRootsFinset p (𝓞 K)) \ {η₀}, 𝔠 η) = 1 := by
+  gcd (𝔭 ^ (m * p)) (∏ η ∈ Finset.attach (nthRootsFinset p (𝓞 K)) \ {η₀}, 𝔠 η) = 1 := by
     rw [← Ideal.isCoprime_iff_gcd]
     apply IsCoprime.pow_left
     rw [Ideal.isCoprime_iff_gcd, hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff,

FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean

@@ -44,21 +44,21 @@ theorem associated_one_sub_pow_primitive_root_of_coprime {n j k : ℕ} {ζ : A}
     exact (this hj).symm.trans (this hk)
   clear k j hk hj
   intro j hj
-  refine associated_of_dvd_dvd ⟨∑ i in range j, ζ ^ i, by rw [← geom_sum_mul_neg, mul_comm]⟩ ?_
+  refine associated_of_dvd_dvd ⟨∑ i ∈ range j, ζ ^ i, by rw [← geom_sum_mul_neg, mul_comm]⟩ ?_
   -- is there an easier way to do this?
   rcases eq_or_ne n 0 with (rfl | hn')
   · simp [j.coprime_zero_right.mp hj]
   rcases eq_or_ne n 1 with (rfl | hn)
   · simp [IsPrimitiveRoot.one_right_iff.mp hζ]
   replace hn := Nat.one_lt_of_ne n hn' hn
   obtain ⟨m, hm⟩ := Nat.exists_mul_emod_eq_one_of_coprime hj hn
-  use ∑ i in range m, (ζ ^ j) ^ i
+  use ∑ i ∈ range m, (ζ ^ j) ^ i
   have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, ←pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
   nth_rw 1 [this]
   rw [← geom_sum_mul_neg, mul_comm]
 
 theorem IsPrimitiveRoot.sum_pow_unit {n k : ℕ} {ζ : A} (hn : 2 ≤ n) (hk : k.Coprime n)
-    (hζ : IsPrimitiveRoot ζ n) : IsUnit (∑ i : ℕ in range k, ζ ^ (i : ℕ)) := by
+    (hζ : IsPrimitiveRoot ζ n) : IsUnit (∑ i ∈ range k, ζ ^ (i : ℕ)) := by
   have h1 : (1 : ℕ).Coprime n := Nat.coprime_one_left n
   have := associated_one_sub_pow_primitive_root_of_coprime _ hζ hk h1
   simp at this
@@ -100,7 +100,7 @@ theorem IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one {p i j : ℕ} {ζ : A}
     rw [hj]
     simp only [tsub_zero]
     exact hi
-  have h3 : IsUnit (-ζ ^ j * ∑ k : ℕ in range (i - j), ζ ^ (k : ℕ)) := by
+  have h3 : IsUnit (-ζ ^ j * ∑ k ∈ range (i - j), ζ ^ (k : ℕ)) := by
     apply IsUnit.mul _ (IsPrimitiveRoot.sum_pow_unit _ hn hic hζ); apply IsUnit.neg
     apply IsUnit.pow; apply hζ.isUnit hp.pos
   obtain ⟨v, hv⟩ := h3
@@ -128,7 +128,7 @@ theorem IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one {p i j : ℕ} {ζ : A}
     rw [hii]
     simp only [tsub_zero]
     exact hj
-  have h3 : IsUnit (ζ ^ i * ∑ k : ℕ in range (j - i), ζ ^ (k : ℕ)) := by
+  have h3 : IsUnit (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ (k : ℕ)) := by
     apply IsUnit.mul _ (IsPrimitiveRoot.sum_pow_unit _ hn hjc hζ); apply IsUnit.pow
     apply hζ.isUnit hp.pos
   obtain ⟨v, hv⟩ := h3

FltRegular/NumberTheory/CyclotomicRing.lean

@@ -116,7 +116,7 @@ lemma nontrivial {p} (hp : p ≠ 0) : Nontrivial (CyclotomicIntegers p) := by
 
 lemma charZero {p} (hp : p ≠ 0) : CharZero (CyclotomicIntegers p) :=
   letI := nontrivial hp
-  ⟨(NoZeroSMulDivisors.algebraMap_injective _ _).comp (algebraMap ℕ ℤ).injective_nat⟩
+  ⟨(FaithfulSMul.algebraMap_injective _ _).comp (algebraMap ℕ ℤ).injective_nat⟩
 
 instance : CharZero (CyclotomicIntegers p) := charZero hpri.out.ne_zero
 

FltRegular/NumberTheory/GaloisPrime.lean

@@ -1,6 +1,6 @@
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.Data.Set.Card
-import Mathlib.FieldTheory.PurelyInseparable
+import Mathlib.FieldTheory.PurelyInseparable.Basic
 import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.SimpleRing.Basic
 import Mathlib.Algebra.Lie.OfAssociative

FltRegular/NumberTheory/Hilbert90.lean

@@ -15,10 +15,10 @@ lemma hφ : ∀ (n : ℕ), φ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n 
 
 variable (η) in
 noncomputable
-def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ ⟨τ, hσ τ⟩), Units.map (σ ^ i) η
+def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i ∈ range (φ ⟨τ, hσ τ⟩), Units.map (σ ^ i) η
 
 include hσ hη in
-lemma aux1 [IsGalois K L] {a: ℕ} (h : a % orderOf σ = 0) : ∏ i in range a, (σ ^ i) η = 1 := by
+lemma aux1 [IsGalois K L] {a: ℕ} (h : a % orderOf σ = 0) : ∏ i ∈ range a, (σ ^ i) η = 1 := by
   obtain ⟨n, hn⟩ := Nat.dvd_iff_mod_eq_zero.2 h
   rw [hn]
   revert a
@@ -44,7 +44,7 @@ lemma aux1 [IsGalois K L] {a: ℕ} (h : a % orderOf σ = 0) : ∏ i in range a,
 
 include hσ hη in
 lemma aux2 [IsGalois K L] {a b : ℕ} (h : a % orderOf σ = b % orderOf σ) :
-    ∏ i in range a, (σ ^ i) η = ∏ i in range b, (σ ^ i) η := by
+    ∏ i ∈ range a, (σ ^ i) η = ∏ i ∈ range b, (σ ^ i) η := by
   wlog hab : b ≤ a generalizing a b
   · exact (this h.symm (not_le.1 hab).le).symm
   obtain ⟨c, hc⟩ := Nat.dvd_iff_mod_eq_zero.2 (Nat.sub_mod_eq_zero_of_mod_eq h)

FltRegular/NumberTheory/Hilbert92.lean

@@ -224,7 +224,7 @@ lemma pow_finEquivZPowers_symm_apply {M} [Group M] (x : M) (hx) (a) :
 lemma norm_eq_prod_pow_gen
     [IsGalois k K] [FiniteDimensional k K]
     (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (η : K) :
-    algebraMap k K (Algebra.norm k η) = (∏ i in Finset.range (orderOf σ), (σ ^ i) η)   := by
+    algebraMap k K (Algebra.norm k η) = (∏ i ∈ Finset.range (orderOf σ), (σ ^ i) η)   := by
   let _ : Fintype (Subgroup.zpowers σ) := inferInstance
   rw [Algebra.norm_eq_prod_automorphisms, ← Fin.prod_univ_eq_prod_range,
     ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
@@ -369,7 +369,7 @@ lemma unit_to_U_div (x y) : mkG (x / y) = mkG x - mkG y := by
   rw [div_eq_mul_inv, unit_to_U_mul, unit_to_U_inv, sub_eq_add_neg]
 
 lemma unit_to_U_prod {ι} (s : Finset ι) (f : ι → _) :
-    mkG (∏ i in s, f i) = ∑ i in s, mkG (f i) := by
+    mkG (∏ i ∈ s, f i) = ∑ i ∈ s, mkG (f i) := by
   classical
   induction s using Finset.induction with
   | empty => simp only [prod_empty, sum_empty, unit_to_U_one]

FltRegular/NumberTheory/Hilbert94.lean

@@ -103,8 +103,8 @@ theorem Ideal.isPrincipal_pow_finrank_of_isPrincipal_map [IsDedekindDomain A] (I
     simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
       (Algebra.lift_rank_eq_of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
         (FractionRing.algEquiv B L).symm.toRingEquiv H).symm
-  rw [← hLK, ← Ideal.spanIntNorm_map, ← (I.map (algebraMap A B)).span_singleton_generator,
-    Ideal.spanIntNorm_singleton]
+  rw [← hLK, ← Ideal.spanNorm_map, ← (I.map (algebraMap A B)).span_singleton_generator,
+    Ideal.spanNorm_singleton]
   exact ⟨⟨_, rfl⟩⟩
 
 /-- This is the first part of **Hilbert Theorem 94**, which states that if `L/K` is an unramified