isIntegralClosure — Mathlib

English

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

Русский

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

LaTeX

$$IsDedekindDomain A$$

Lean4

theorem isIntegralClosure (B : Type*) [CommRing B] [IsDomain B] [Nontrivial R] [Algebra R A] [Algebra R B] [Algebra B A]
    [IsScalarTower R B A] [IsIntegralClosure B R A] [DimensionLEOne R] : DimensionLEOne B where
  maximalOfPrime := fun {p} ne_bot _ =>
    IsIntegralClosure.isMaximal_of_isMaximal_comap (R := R) A p
      (Ideal.IsPrime.isMaximal inferInstance (IsIntegralClosure.comap_ne_bot A ne_bot))

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