Module docstring
{"# Integral algebras
Main definitions
Let R be a CommRing and let A be an R-algebra.
Algebra.IsIntegral R A: An algebra is integral if every element of the extension is integral over the base ring. "}
Algebra.IsIntegral
structure
Full source
/-- An algebra is integral if every element of the extension is integral over the base ring. -/
protected class Algebra.IsIntegral : Prop where
isIntegral : ∀ x : A, IsIntegral R xInformal description
An $R$-algebra $A$ is called integral if every element $x \in A$ is integral over $R$, meaning that for each $x \in A$, there exists a monic polynomial $p \in R[X]$ such that $p(x) = 0$.
Algebra.isIntegral_def
theorem
: Algebra.IsIntegral R A ↔ ∀ x : A, IsIntegral R x
Informal description
An $R$-algebra $A$ is integral if and only if every element $x \in A$ is integral over $R$.