Theorems · Definition · commutative algebra

integralClosure

(R : Type u_1) → (A : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → Subalgebra R A

The integral closure of R in an R-algebra A.

Defined in

Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Cited by

105 results in Mathlib

Foundations

Depth 135 from the axioms, rests on 4,344 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra