mathlib

ee863ec1 - feat(ring_theory/algebraic): algebraic extensions, algebraic elements (#1519)

feat(ring_theory/algebraic): algebraic extensions, algebraic elements (#1519) * chore(ring_theory/algebra): make first type argument explicit in alg_hom Now this works, and it didn't work previously even with `@` ```lean structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ] [algebra α β] [algebra α γ] extends alg_hom α β γ := ``` * Update algebra.lean * feat(field_theory/algebraic_closure) * Remove sorries about minimal polynomials * Define alg_equiv.symm * typo * Remove another sorry, in base_extension * Work in progress * Remove a sorry in maximal_extension_chain * Merge two sorries * More sorries removed * More work on transitivity of algebraicity * WIP * Sorry-free definition of algebraic closure * More or less sorries * Removing some sorries * WIP * Fix algebraic.lean * Fix build, mostly * Remove stuff about UMP of alg clos * Prove transitivity of algebraic extensions * Add some docstrings * Remove files with stuff for future PRs * Add a bit to the module docstring * Fix module docstring * Include assumption in section injective * Aesthetic changes to is_integral_of_mem_of_fg * Little improvements of proofs in algebraic.lean * Improve some proofs in integral_closure.lean * Make variable name explicit * Process comments