Commit 2019-09-26 13:55 3cd33416
View on Github →feat(field_theory/minimal_polynomial): Basics on minimal polynomials (#1449)
- 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
- feat(field_theory/minimal_polynomial): Basics on minimal polynomials
- Remove protected; add docstrings
- Open classical locale
- Stuff is broken
- Rewrite the module doc a bit, revert change to classical
- Little fixes
- explicit-ify proof
- feat(algebra/big_operators): simp lemmas
- Remove decidable_eq instances
- fix(ring_theory/algebra): get ris of dec_eq assumptions so simp triggers again
- break as_sum into its constituent pieces
- fix namespace
- not sure if this is better or worse
- Fix ext naming
- More fixes
- Fix some renaming issues