instIsIntegralClosure — Mathlib

English

If R is integrally closed, then the integral closure relation lifts to K: IsIntegralClosure R R K holds.

Русский

Если R интегрально замкнуто, то всякая интегральность над R в K сохраняется: IsIntegralClosure R R K.

LaTeX

$$$IsIntegralClosure\,R\,R\,K$ under IsIntegrallyClosed R (as an instance).$$

Lean4

/-- Note that this is not a duplicate instance, since `IsIntegrallyClosed R` is instead defined
as `IsIntegrallyClosed R R (FractionRing R)`. -/
instance [iic : IsIntegrallyClosed R] : IsIntegralClosure R R K :=
  (isIntegrallyClosed_iff_isIntegralClosure K).mp iic

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