feat: port RingTheory.Etale (#5781)

Co-authored-by: Matthew Ballard <matt@mrb.email>
leanprover-community · Jul 10, 2023 · 888c409 · 888c409
1 parent d2aa4e1
commit 888c409
Show file tree

Hide file tree

Showing 3 changed files with 592 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2689,6 +2689,7 @@ import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.DiscreteValuationRing.TFAE
 import Mathlib.RingTheory.Discriminant
 import Mathlib.RingTheory.EisensteinCriterion
+import Mathlib.RingTheory.Etale
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Filtration
 import Mathlib.RingTheory.FinitePresentation