feat: port RingTheory.ChainOfDivisors (#3056)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
leanprover-community · May 10, 2023 · f4af9a6 · f4af9a6
1 parent a87ba08
commit f4af9a6
Show file tree

Hide file tree

Showing 2 changed files with 477 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1561,6 +1561,7 @@ import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Adjoin.Fg
 import Mathlib.RingTheory.Adjoin.Tower
 import Mathlib.RingTheory.AlgebraTower
+import Mathlib.RingTheory.ChainOfDivisors
 import Mathlib.RingTheory.Congruence
 import Mathlib.RingTheory.Coprime.Basic
 import Mathlib.RingTheory.Coprime.Ideal