Skip to content

Commit fb4aed5

Browse files
Parcly-Taxelkim-em
andcommitted
chore: delete deprecated algebraic structure files (#16836)
Based on a comparison with 32de3f6 these six files have not been substantially changed for over a year. Co-authored-by: Kim Morrison <kim@tqft.net>
1 parent f7efa03 commit fb4aed5

File tree

8 files changed

+1
-1893
lines changed

8 files changed

+1
-1893
lines changed

Mathlib.lean

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3086,19 +3086,13 @@ import Mathlib.Deprecated.Cardinal.Finite
30863086
import Mathlib.Deprecated.Cardinal.PartENat
30873087
import Mathlib.Deprecated.Combinator
30883088
import Mathlib.Deprecated.Equiv
3089-
import Mathlib.Deprecated.Group
30903089
import Mathlib.Deprecated.HashMap
30913090
import Mathlib.Deprecated.LazyList
30923091
import Mathlib.Deprecated.Logic
30933092
import Mathlib.Deprecated.MinMax
30943093
import Mathlib.Deprecated.NatLemmas
30953094
import Mathlib.Deprecated.Order
30963095
import Mathlib.Deprecated.RelClasses
3097-
import Mathlib.Deprecated.Ring
3098-
import Mathlib.Deprecated.Subfield
3099-
import Mathlib.Deprecated.Subgroup
3100-
import Mathlib.Deprecated.Submonoid
3101-
import Mathlib.Deprecated.Subring
31023096
import Mathlib.Dynamics.BirkhoffSum.Average
31033097
import Mathlib.Dynamics.BirkhoffSum.Basic
31043098
import Mathlib.Dynamics.BirkhoffSum.NormedSpace

0 commit comments

Comments
 (0)