Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor: turn
DimensionLEOne
into a class (#5833)
The predicate that a ring has Krull dimension at most one was a regular `def`. I believe we should turn it into a class because: * The property follows from the ring structure, e.g. because it is a PID or because it is an integral closure. * We pass it around as a whole hypothesis, something instance synthesis can deal well with. * It makes the definition of `IsDedekindDomain` the conjunction of a number of classes, so we could switch to `extends` for all its fields. The main change in API is the addition of `Ideal.IsPrime.isMaximal` which is a restatement of the Krull dimension property with convenient dot notation: turn a prime ideal into a maximal ideal given the hypothesis that it's not zero. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60IsDedekindDomain.60.20extend.20.60IsDomain.60.3F/near/374515392
- Loading branch information
1 parent
898a8e7
commit f5c15b3
Showing
5 changed files
with
41 additions
and
34 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters