Skip to content

Commit 876313a

Browse files
ROTARTSI82ROTARTSI82
committed
Revert "feat(LocalRing/Etale): Finite etale extensions are monogenic"
This reverts commit cc73956.
1 parent 5823012 commit 876313a

2 files changed

Lines changed: 0 additions & 173 deletions

File tree

‎Mathlib.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6406,7 +6406,6 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
64066406
public import Mathlib.RingTheory.LocalProperties.Submodule
64076407
public import Mathlib.RingTheory.LocalRing.Basic
64086408
public import Mathlib.RingTheory.LocalRing.Defs
6409-
public import Mathlib.RingTheory.LocalRing.Etale
64106409
public import Mathlib.RingTheory.LocalRing.LocalSubring
64116410
public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
64126411
public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs

‎Mathlib/RingTheory/LocalRing/Etale.lean‎

Lines changed: 0 additions & 172 deletions
This file was deleted.

0 commit comments

Comments
 (0)