@[reducible, inline]

abbrev isIntegral_def (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (b : B) : Prop

@[reducible, inline]

abbrev integralClosureSubalgebra (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] : Subalgebra A B

theorem isIntegral_add_and_mul {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {α β : B} (hα : IsIntegral A α) (hβ : IsIntegral A β) : IsIntegral A (α + β) ∧ IsIntegral A (α * β)

theorem proposition_1_20 {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (hAB : Algebra.IsIntegral A B) (hBC : Algebra.IsIntegral B C) : Algebra.IsIntegral A C

theorem corollary_1_21' (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] : IsIntegrallyClosedIn (↥(integralClosure A B)) B

theorem proposition_1_22 : IsIntegrallyClosed ℤ

theorem corollary_1_23 (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] : IsIntegrallyClosed A

theorem proposition_1_25 (A : Type u_1) [CommRing A] [IsDomain A] [ValuationRing A] : IsIntegrallyClosed A

theorem proposition_1_28 {A : Type u_1} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] {α : L} (hα : IsAlgebraic K α) : IsIntegral A α ↔ ∀ (i : ℕ), (minpoly K α).coeff i ∈ (algebraMap A K).range