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.

class Algebra.IsIntegral (R : Type u_1) (A : Type u_3) [CommRing R] [Ring A] [Algebra R A] : Prop

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

• isIntegral (x : A) : IsIntegral R x

theorem Algebra.isIntegral_iff (R : Type u_1) (A : Type u_3) [CommRing R] [Ring A] [Algebra R A] : Algebra.IsIntegral R A ↔ ∀ (x : A), IsIntegral R x

theorem Algebra.isIntegral_def {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] : Algebra.IsIntegral R A ↔ ∀ (x : A), IsIntegral R x

theorem algebraMap_isIntegral_iff {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] : (algebraMap R A).IsIntegral ↔ Algebra.IsIntegral R A