theorem FieldExtensions.tower_law (F : Type u_1) (E : Type u_2) (K : Type u_3) [Field F] [Field E] [Field K] [Algebra F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] [FiniteDimensional F E] [FiniteDimensional E K] : FiniteDimensional F K ∧ Module.finrank F K = Module.finrank F E * Module.finrank E K

theorem FieldExtensions.finiteDimensional_tower_iff (K : Type u_1) (F : Type u_2) (E : Type u_3) [Field K] [Field F] [Field E] [Algebra K F] [Algebra F E] [Algebra K E] [IsScalarTower K F E] : Module.finrank K F * Module.finrank F E = Module.finrank K E ∧ (FiniteDimensional K E ↔ FiniteDimensional K F ∧ FiniteDimensional F E)

theorem FieldExtensions.algebraic_operations {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {α β : L} (hα : IsAlgebraic K α) (hβ : IsAlgebraic K β) : IsAlgebraic K (α + β) ∧ IsAlgebraic K (α * β) ∧ IsAlgebraic K (α / β)

theorem FieldExtensions.isAlgebraic_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) : IsAlgebraic K α ↔ ∃ (p : Polynomial K), p ≠ 0 ∧ (Polynomial.aeval α) p = 0

theorem FieldExtensions.isAlgebraic_iff_adjoin_finiteDimensional {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) : IsAlgebraic K α ↔ FiniteDimensional K ↥K⟮α⟯