Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-16 21:40 ee863ec1

View on Github →

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

Estimated changes