From b0eb9f8b6b0e642ae7df8886ebcd033f779746f8 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Wed, 23 Oct 2024 17:26:40 +0200 Subject: [PATCH] shake --- FltRegular/NumberTheory/AuxLemmas.lean | 5 ++--- FltRegular/NumberTheory/Finrank.lean | 1 - FltRegular/NumberTheory/GaloisPrime.lean | 4 ++++ 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index 57f71842..d10011f1 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -1,10 +1,9 @@ import Mathlib.NumberTheory.RamificationInertia import Mathlib.Algebra.Polynomial.Taylor -import Mathlib.RingTheory.Valuation.ValuationRing import Mathlib.FieldTheory.Separable import Mathlib.RingTheory.Trace.Defs - -import Mathlib +import Mathlib.Algebra.Lie.OfAssociative +import Mathlib.RingTheory.SimpleRing.Basic /-! diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean index 7ae6492b..b28bc476 100644 --- a/FltRegular/NumberTheory/Finrank.lean +++ b/FltRegular/NumberTheory/Finrank.lean @@ -2,7 +2,6 @@ import Mathlib.LinearAlgebra.Dimension.Constructions import Mathlib.LinearAlgebra.Dimension.Finite import Mathlib.Algebra.Module.Torsion import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition -import Mathlib.LinearAlgebra.FreeModule.PID import Mathlib.LinearAlgebra.Dimension.Localization open Module diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean index bbdf79af..034b826a 100644 --- a/FltRegular/NumberTheory/GaloisPrime.lean +++ b/FltRegular/NumberTheory/GaloisPrime.lean @@ -1,6 +1,10 @@ import FltRegular.NumberTheory.AuxLemmas import Mathlib.RingTheory.IntegralClosure.IntegralRestrict import Mathlib.Data.Set.Card +import Mathlib.FieldTheory.PurelyInseparable +import Mathlib.Order.CompletePartialOrder +import Mathlib.RingTheory.DedekindDomain.Dvr +import Mathlib.Algebra.Order.Star.Basic /-! # Galois action on primes