Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 6e7ca69

Browse files
VierkantorVierkantor
committed
chore(ring_theory): split finiteness into finite, finite type and finite presentation (#17481)
`module.finite` is used in a lot of places (especially in the form of `finite_dimensional`) but it is defined alongside `algebra.finite_type` and `algebra.finite_presentation`, so it brings a lot of dependencies with it. By splitting the file along the lines of the three definitions we should be able to clean up the import graph noticeably. In particular, finite dimensional vector spaces shouldn't know about (`mv_`)polynomials anymore.
1 parent 597343b commit 6e7ca69

11 files changed

Lines changed: 1112 additions & 958 deletions

File tree

‎src/data/polynomial/module.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Andrew Yang
55
-/
66

7-
import ring_theory.finiteness
7+
import ring_theory.finite_type
88

99
/-!
1010
# Polynomial module

‎src/linear_algebra/finite_dimensional.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Chris Hughes
66
import algebra.algebra.subalgebra.basic
77
import field_theory.finiteness
88
import linear_algebra.finrank
9+
import tactic.interval_cases
910

1011
/-!
1112
# Finite dimensional vector spaces

‎src/ring_theory/adjoin_root.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ import algebra.algebra.basic
77
import data.polynomial.field_division
88
import linear_algebra.finite_dimensional
99
import ring_theory.adjoin.basic
10+
import ring_theory.finite_presentation
11+
import ring_theory.finite_type
1012
import ring_theory.power_basis
1113
import ring_theory.principal_ideal_domain
1214

‎src/ring_theory/finite_presentation.lean‎

Lines changed: 454 additions & 0 deletions
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)