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.isIntegral {R : Type u_1} {A : Type u_3} : ∀ {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A} [self : 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