Theorems · Inductive type · commutative algebra

IsIntegralClosure

(A : Type u_1) →
  (R : Type u_2) →
    (B : Type u_3) →
      [inst : CommRing R] → [inst_1 : CommSemiring A] → [inst_2 : CommRing B] → [Algebra R B] → [Algebra A B] → Prop

IsIntegralClosure A R B is the characteristic predicate stating A is the integral closure of R in B, i.e. that an element of B is integral over R iff it is an element of (the image of) A.

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs

Cited by

146 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 22 definitions · uses no axioms

Assumes

CommRingCommSemiringCommRingAlgebraAlgebra