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