Theorems · Definition · commutative algebra

RingHom.IsIntegralElem

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

An element x of A is said to be integral over R with respect to f if it is a root of a monic polynomial p : R[X] evaluated under f

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

Cited by

33 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRing