isDedekindDomain — Mathlib

English

If A is a domain and a principal ideal ring, then A is a Dedekind domain.

Русский

Если A — область и кольцо с единичными идеалами, то A является Дедекиндовым кольцом.

LaTeX

$$IsDedekindDomain A$$

Lean4

instance (priority := 100) isDedekindDomain [IsDomain A] [IsPrincipalIdealRing A] : IsDedekindDomain A :=
  { PrincipalIdealRing.isNoetherianRing, Ring.DimensionLEOne.principal_ideal_ring A,
    UniqueFactorizationMonoid.instIsIntegrallyClosed with }

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