Skip to content

Commit 45edb79

Browse files
chore(RingTheory/ClassGroup): deprecate module (leanprover-community#40157)
Follow-up for leanprover-community#38127.
1 parent 22c29ac commit 45edb79

2 files changed

Lines changed: 11 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6399,6 +6399,7 @@ public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
63996399
public import Mathlib.RingTheory.Bialgebra.TensorProduct
64006400
public import Mathlib.RingTheory.Binomial
64016401
public import Mathlib.RingTheory.ChainOfDivisors
6402+
public import Mathlib.RingTheory.ClassGroup
64026403
public import Mathlib.RingTheory.ClassGroup.Basic
64036404
public import Mathlib.RingTheory.ClassGroup.ExtendedHom
64046405
public import Mathlib.RingTheory.Coalgebra.Basic

Mathlib/RingTheory/ClassGroup.lean

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
/-
2+
Copyright (c) 2021 Anne Baanen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Anne Baanen
5+
-/
6+
module -- shake: keep-all
7+
8+
public import Mathlib.RingTheory.ClassGroup.Basic
9+
10+
deprecated_module (since := "2026-06-02")

0 commit comments

Comments
 (0)