bump

FltRegular/CaseII/InductionStep.lean

@@ -9,17 +9,15 @@ variable {K : Type*} {p : ℕ+} [Field K] (hp : p ≠ 2)
 
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) {x y z : 𝓞 K} {ε : (𝓞 K)ˣ}
 
-attribute [local instance 2000] CommRing.toRing Semiring.toNonUnitalSemiring
-  NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid
+attribute [local instance 2000] Semiring.toNonUnitalSemiring
+  NonUnitalSemiring.toNonUnitalNonAssocSemiring
 
-set_option quotPrecheck false
 local notation3 "π" => Units.val (IsPrimitiveRoot.unit' hζ) - 1
 local notation3 "𝔭" => Ideal.span {π}
 local notation3 "𝔦" η => Ideal.span {(x + y * η : 𝓞 K)}
 local notation3 "𝔵" => Ideal.span {x}
 local notation3 "𝔶" => Ideal.span {y}
 local notation3 "𝔷" => Ideal.span {z}
-local notation3 "𝔪" => gcd 𝔵 𝔶
 
 variable {m : ℕ} (e : x ^ (p : ℕ) + y ^ (p : ℕ) = ε * ((hζ.unit'.1 - 1) ^ (m + 1) * z) ^ (p : ℕ))
 variable (hy : ¬ hζ.unit'.1 - 1 ∣ y) (hz : ¬ hζ.unit'.1 - 1 ∣ z)
@@ -47,6 +45,8 @@ lemma span_pow_add_pow_eq :
 
 variable [NumberField K]
 
+local notation3 "𝔪" => gcd 𝔵 𝔶
+
 include hy in
 lemma m_ne_zero : 𝔪 ≠ 0 := by
   simp_rw [Ne, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -115,7 +115,7 @@ open IsPrimitiveRoot
 theorem nth_roots_prim [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) :
     IsPrimitiveRoot η p := by
   have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe
-  rw [nthRoots_one_eq_biUnion_primitiveRoots' hζ'] at hη
+  rw [nthRoots_one_eq_biUnion_primitiveRoots hζ'] at hη
   simp only [mem_biUnion] at hη
   obtain ⟨a, ha, h2⟩ := hη
   have ha2 : a = p := by
@@ -166,7 +166,7 @@ theorem diff_of_roots [hp : Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ :
     (hwlog : η₁ ≠ 1) : ∃ u : Rˣ, η₁ - η₂ = u * (1 - η₁) := by
   replace ph : 2 ≤ p := le_trans (by decide) ph
   have h := nth_roots_prim hη₁ hwlog
-  obtain ⟨i, ⟨H, hi⟩⟩ := h.eq_pow_of_pow_eq_one ((mem_nthRootsFinset hp.out.pos).1 hη₂) hp.out.pos
+  obtain ⟨i, ⟨H, hi⟩⟩ := h.eq_pow_of_pow_eq_one ((mem_nthRootsFinset hp.out.pos).1 hη₂)
   have hi1 : 1 ≠ i := by
     intro hi1
     rw [← hi1, pow_one] at hi

FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean

@@ -5,7 +5,7 @@ Authors: Alex J. Best
 
 ! This file was ported from Lean 3 source module number_theory.cyclotomic.cyclotomic_units
 -/
-import Mathlib.RingTheory.RootsOfUnity.Basic
+import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
 
 noncomputable section
 
@@ -144,10 +144,11 @@ lemma IsPrimitiveRoot.associated_sub_one {A : Type*} [CommRing A] [IsDomain A]
     {p : ℕ} (hp : p.Prime) {ζ : A} (hζ : IsPrimitiveRoot ζ p) {η₁ : A}
     (hη₁ : η₁ ∈ nthRootsFinset p A) {η₂ : A} (hη₂ : η₂ ∈ nthRootsFinset p A) (e : η₁ ≠ η₂) :
     Associated (ζ - 1) (η₁ - η₂) := by
+  have : NeZero p := ⟨hp.ne_zero⟩
   obtain ⟨i, ⟨hi, rfl⟩⟩ :=
-    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₁) hp.pos
+    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₁)
   obtain ⟨j, ⟨hj, rfl⟩⟩ :=
-    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₂) hp.pos
+    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₂)
   have : i ≠ j := ne_of_apply_ne _ e
   obtain ⟨u, h⟩ := CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one A
     hp.two_le hp hi hj this hζ

FltRegular/NumberTheory/Cyclotomic/Factoring.lean

@@ -47,7 +47,8 @@ theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul (hpos : 0 < n) (h : IsPrimitiveR
   · rw [mem_nthRootsFinset hpos, ← map_pow, (mem_nthRootsFinset hpos).1 ha, map_one]
   · rw [mem_coe, mem_nthRootsFinset hpos] at ha
     simp only [Set.mem_image, mem_coe]
-    obtain ⟨i, -, hζ⟩ := h'.eq_pow_of_pow_eq_one ha hpos
+    have : NeZero n := ⟨hpos.ne'⟩
+    obtain ⟨i, -, hζ⟩ := h'.eq_pow_of_pow_eq_one ha
     refine ⟨ζ ^ i, ?_, by rwa [map_pow]⟩
     rw [mem_nthRootsFinset hpos, ← pow_mul, mul_comm, pow_mul, h.pow_eq_one, one_pow]
 

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -38,7 +38,7 @@ theorem galConj_zeta : galConj K p (zeta p ℚ K) = (zeta p ℚ K)⁻¹ := by
 include hζ in
 @[simp]
 theorem galConj_zeta_runity : galConj K p ζ = ζ⁻¹ := by
-  obtain ⟨t, _, rfl⟩ := (zeta_spec p ℚ K).eq_pow_of_pow_eq_one hζ.pow_eq_one p.pos
+  obtain ⟨t, _, rfl⟩ := (zeta_spec p ℚ K).eq_pow_of_pow_eq_one hζ.pow_eq_one
   rw [map_pow, galConj_zeta, inv_pow]
 
 include hζ in

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -65,24 +65,22 @@ theorem contains_two_primitive_roots {p q : ℕ} {x y : K} [FiniteDimensional 
   have hkpos : 0 < k := Nat.pos_of_ne_zero (Nat.lcm_ne_zero hppos.ne' hqpos.ne')
   let xu := IsUnit.unit (hx.isUnit hppos)
   let yu := IsUnit.unit (hy.isUnit hqpos)
-  have hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K :=  by
-    rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
-      IsUnit.unit_spec]
+  have hxmem : xu ∈ rootsOfUnity k K :=  by
+    rw [mem_rootsOfUnity, ← Units.val_eq_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec]
     exact (hx.pow_eq_one_iff_dvd _).2 (dvd_lcm_left _ _)
-  have hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K := by
-    rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
-      IsUnit.unit_spec]
+  have hymem : yu ∈ rootsOfUnity k K := by
+    rw [mem_rootsOfUnity, ← Units.val_eq_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec]
     exact (hy.pow_eq_one_iff_dvd _).2 (dvd_lcm_right _ _)
-  have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = p := by
-    rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
+  have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity k K) = p := by
+    rw [← orderOf_injective (rootsOfUnity k K).subtype Subtype.coe_injective,
       Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
     exact hx.eq_orderOf.symm
-  have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = q := by
-    rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
+  have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity k K) = q := by
+    rw [← orderOf_injective (rootsOfUnity k K).subtype Subtype.coe_injective,
       Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
     exact hy.eq_orderOf.symm
-  obtain ⟨g : rootsOfUnity ⟨k, hkpos⟩ K, hg⟩ :=
-    IsCyclic.exists_monoid_generator (α := rootsOfUnity ⟨k, hkpos⟩ K)
+  have : NeZero k := ⟨hkpos.ne'⟩
+  obtain ⟨g : rootsOfUnity k K, hg⟩ := IsCyclic.exists_monoid_generator (α := rootsOfUnity k K)
   obtain ⟨nx, hnx⟩ := hg ⟨xu, hxmem⟩
   obtain ⟨ny, hny⟩ := hg ⟨yu, hymem⟩
   have H : orderOf g = k := by
@@ -123,7 +121,7 @@ theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type*} [CommRing A] [IsDomain
     (hζ : IsPrimitiveRoot ζ p) {μ : A} (hμ : μ ^ (p : ℕ) = 1) :
     (@DFunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1}) _
       (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ) = 1 := by
-  obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
+  obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ
   rw [map_pow, eq_one_mod_one_sub, one_pow]
 
 set_option synthInstance.maxHeartbeats 80000 in
@@ -232,7 +230,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
       simp only [one_pow]
       apply hxp'
     cases' hxp'' with hxp'' hxp''
-    · obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop
+    · obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp''
       refine ⟨i, 2, ?_⟩
       rw [← Subtype.val_inj] at Hi
       simp only [SubmonoidClass.coe_pow] at Hi
@@ -243,7 +241,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
       have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by
         rw [mul_pow, hone, hxp'']
         ring
-      obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp3 p.prop
+      obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp3
       refine ⟨i, 1, ?_⟩
       simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg]
       rw [← Subtype.val_inj] at Hi
@@ -376,5 +374,5 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u :
 lemma IsPrimitiveRoot.eq_one_mod_one_sub' {A : Type*} [CommRing A] [IsDomain A]
     {n : ℕ+} {ζ : A} (hζ : IsPrimitiveRoot ζ n) {η : A} (hη : η ∈ nthRootsFinset n A) :
     Ideal.Quotient.mk (Ideal.span ({ζ - 1} : Set A)) η = 1 := by
-  obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2).1 hη) n.2
+  obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2).1 hη)
   rw [map_pow, ← Ideal.Quotient.algebraMap_eq, eq_one_mod_one_sub, one_pow]

FltRegular/NumberTheory/GaloisPrime.lean

@@ -247,7 +247,10 @@ lemma Ideal.inertiaDegIn_bot [Nontrivial R] [IsDomain S] [NoZeroSMulDivisors R S
   letI : Field R := hR.toField
   letI : Field S := hS.toField
   rw [← Ideal.map_bot (f := algebraMap R S), ← finrank_quotient_map (R := R) (S := S) ⊥ R S]
-  exact inertiaDeg_algebraMap _ _
+  convert inertiaDeg_algebraMap _ _
+  simp only [map_bot]
+  exact ⟨(comap_bot_of_injective _
+    (NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance)).symm⟩
 
 variable {R S}
 
@@ -261,7 +264,7 @@ lemma Ideal.ramificationIdxIn_eq_ramificationIdx [IsGalois K L] (p : Ideal R) (P
   rw [dif_pos this]
   have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S hP this.choose_spec
   rw [← hσ]
-  exact Ideal.ramificationIdx_comap_eq (galRestrict R K L S σ) P
+  exact Ideal.ramificationIdx_comap_eq _ (galRestrict R K L S σ) P
 
 lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S)
     (hP : P ∈ primesOver S p) [p.IsMaximal] :

FltRegular/NumberTheory/Hilbert90.lean

@@ -1,6 +1,5 @@
 
 import Mathlib.RingTheory.SimpleModule
-import Mathlib.RingTheory.Valuation.ValuationRing
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.Tactic.Widget.Conv

FltRegular/NumberTheory/Hilbert92.lean

@@ -710,10 +710,6 @@ lemma IsPrimitiveRoot.coe_coe_iff {ν : (𝓞 k)ˣ} {n} :
     (f := (algebraMap (𝓞 k) k).toMonoidHom.comp (Units.coeHom (𝓞 k)))
     ((IsFractionRing.injective (𝓞 k) k).comp Units.ext)
 
-lemma Subgroup.isCyclic_of_le {M : Type*} [Group M] {H₁ H₂ : Subgroup M} [IsCyclic H₂]
-    (e : H₁ ≤ H₂) : IsCyclic H₁ :=
-  isCyclic_of_surjective _ (subgroupOfEquivOfLe e).surjective
-
 include hp in
 lemma h_exists' : ∃ (h : ℕ) (ν : (𝓞 k)ˣ),
     IsPrimitiveRoot (ν : k) (p ^ h) ∧
@@ -832,7 +828,8 @@ lemma almostHilbert92 (hpodd : (p : ℕ) ≠ 2) :
           Units.coe_map_inv, MonoidHom.coe_coe, SubmonoidClass.coe_pow, Submonoid.coe_mul,
           Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, Units.val_one,
           OneMemClass.coe_one, RingOfInteger.coe_algebraMap_apply] at NE_p_pow
-        obtain ⟨i, -, e⟩ := hν''.eq_pow_of_pow_eq_one NE_p_pow p.pos
+        have : NeZero p.1 := ⟨hp.pos.ne'⟩
+        obtain ⟨i, -, e⟩ := hν''.eq_pow_of_pow_eq_one NE_p_pow
         use ((ν ^ (p : ℕ) ^ h) ^ i * ε')
         rw [map_mul, ← mul_inv_eq_iff_eq_mul]
         ext

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -299,12 +299,12 @@ include hu hp hζ hcong in
 attribute [local instance] Ideal.Quotient.field in
 lemma isUnramified (L) [Field L] [Algebra K L] [IsSplittingField K L (X ^ (p : ℕ) - C (u : K))] :
     IsUnramified (𝓞 K) (𝓞 L) := by
-  let α := polyRoot hp hζ u hcong _ (rootOfSplitsXPowSubC_pow p.pos _ L) 0
+  let α := polyRoot hp hζ u hcong _ (rootOfSplitsXPowSubC_pow _ L) 0
   haveI := Polynomial.IsSplittingField.finiteDimensional L (X ^ (p : ℕ) - C (u : K))
   have hα : Algebra.adjoin K {(α : L)} = ⊤ := by
     rw [eq_top_iff, ← Algebra.adjoin_root_eq_top_of_isSplittingField
       ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu)
-      (rootOfSplitsXPowSubC_pow p.pos (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
+      (rootOfSplitsXPowSubC_pow (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
     exact mem_adjoin_polyRoot hp hζ u hcong _ _ 0
   constructor
   intros I hI hIbot

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb6c831c05bc6ca6d37454ca97531a9b780dfcb5",
+   "rev": "af731107d531b39cd7278c73f91c573f40340612",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
+   "rev": "93bcfd774f89d3874903cab06abfbf69f327cbd9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,17 +35,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.43",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0ea83a676d288220ba227808568cbb80fe43ace0",
+   "rev": "ac7b989cbf99169509433124ae484318e953d201",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d27f22898a74975360dd1387155c6031b501a90b",
+   "rev": "c9fc36ea39408920f0afb0700715df51bee95f84",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
+   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
+   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d36b7fd4c730cae8a3a8edfe98beb34ef0fc6e0a",
+   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:v4.14.0-rc2