isDedekindDomain_iff_isDedekindDomainInv

English

IsDedekindDomain A is equivalent to IsDedekindDomainInv A for domains A (with IsDomain).

Русский

IsDedekindDomain A эквивалентен IsDedekindDomainInv A для областей A.

LaTeX

$$$$\\text{IsDedekindDomain}(A) \\iff \\text{IsDedekindDomainInv}(A).$$$$

Lean4

/-- `IsDedekindDomain` and `IsDedekindDomainInv` are equivalent ways
to express that an integral domain is a Dedekind domain. -/
theorem isDedekindDomain_iff_isDedekindDomainInv [IsDomain A] : IsDedekindDomain A ↔ IsDedekindDomainInv A :=
  ⟨fun _h _I hI => FractionalIdeal.mul_inv_cancel hI, fun h => h.isDedekindDomain⟩

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