Commit 2019-10-16 21:40 ee863ec1

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 @

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