Theorems · Inductive type · commutative algebra

Algebra.IsIntegral

(R : Type u_1) → (A : Type u_3) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Prop

An algebra is integral if every element of the extension is integral over the base ring.

Defined in

Mathlib.RingTheory.IntegralClosure.Algebra.Defs

Cited by

224 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebra