Theorems · Definition · commutative algebra

IsIntegral

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

An element x of an algebra A over a commutative ring R is said to be integral, if it is a root of some monic polynomial p : R[X]. Equivalently, the element is integral over R with respect to the induced algebraMap

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

Cited by

427 results in Mathlib

Foundations

Depth 66 from the axioms, rests on 1,018 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra