instIsDedekindDomainOfIsDomainOfIsDedekindRing

English

If B is the integral closure of R in A and R satisfies certain properties, then B inherits a dimension ≤ 1 property.

Русский

Если B — интегральное замыкание R в A и R удовлетворяет условиям, то B наследует свойство размерности ≤ 1.

LaTeX

$$DimensionLEOne B$$

Lean4

/-- Make a Dedekind domain from a Dedekind ring given that it is a domain.

`IsDedekindRing` and `IsDedekindDomain` form a cycle in the typeclass hierarchy:
`IsDedekindRing R + IsDomain R` imply `IsDedekindDomain R`, which implies `IsDedekindRing R`.
This should be safe since the start and end point is the literal same expression,
which the tabled typeclass synthesis algorithm can deal with.
-/
instance [IsDomain A] [IsDedekindRing A] : IsDedekindDomain A where

Похожие утверждения