bump

Author: riccardobrasca

FltRegular.lean

@@ -10,7 +10,6 @@ import FltRegular.NumberTheory.Cyclotomic.CyclRat
 import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.CyclotomicRing
-import FltRegular.NumberTheory.GaloisPrime
 import FltRegular.NumberTheory.Hilbert90
 import FltRegular.NumberTheory.Hilbert92
 import FltRegular.NumberTheory.Hilbert94

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -66,13 +66,6 @@ theorem mem_fltIdeals [Fact p.Prime] (x y : ℤ) {η : R} (hη : η ∈ nthRoots
     ↑x + η * ↑y ∈ fltIdeals p x y hη :=
   mem_span_singleton.mpr dvd_rfl
 
-theorem Ideal.le_add {S : Type*} [CommRing S] (a b c d : Ideal S) (hab : a ≤ b) (hcd : c ≤ d) :
-    a + c ≤ b + d := by
-  simp only [Submodule.add_eq_sup, sup_le_iff]
-  constructor
-  · apply le_trans hab (@le_sup_left _ _ _ _)
-  · apply le_trans hcd (@le_sup_right _ _ _ _)
-
 open IsPrimitiveRoot
 
 theorem prim_coe (ζ : R) (hζ : IsPrimitiveRoot ζ p) : IsPrimitiveRoot (ζ : CyclotomicField p ℚ) p :=

FltRegular/NumberTheory/GaloisPrime.lean

@@ -1,7 +1,6 @@
-import FltRegular.NumberTheory.GaloisPrime
 import Mathlib.RingTheory.DedekindDomain.Different
 import Mathlib.Order.CompletePartialOrder
-import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.NumberTheory.RamificationInertia.Galois
 
 /-!
 # Unramified extensions

FltRegular/NumberTheory/Unramified.lean

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "63c92d89bf2723c770ea68f7f99885a44a302249",
+   "rev": "915cd38ee571dc4dac8c536ff191c397abf53a5c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,