Commit 2023-07-24 07:23 f5c15b35

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