feat: port RingTheory.ClassGroup (#4732)

Some proofs are really slow and need a lot of heartbeats to complete (up to 600000). Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Jun 7, 2023 · 549bb59 · 549bb59
1 parent 55822ef
commit 549bb59
Show file tree

Hide file tree

Showing 2 changed files with 421 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2280,6 +2280,7 @@ import Mathlib.RingTheory.AlgebraicIndependent
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Bezout
 import Mathlib.RingTheory.ChainOfDivisors
+import Mathlib.RingTheory.ClassGroup
 import Mathlib.RingTheory.Congruence
 import Mathlib.RingTheory.Coprime.Basic
 import Mathlib.RingTheory.Coprime.Ideal