Commit 2024-11-07 05:22 ab7a60c7
View on Github →feat(Algebra): misc lemmas and cleanup (#18431)
- In IsAlgClosed/Basic we add the fact that an algebraic extension E/F is an algebraic closure if all (monic irreducible) polynomials in F[X] split in E. In fact it suffices that every such polynomial has a root in E, but is used to deduce the "split" version in #18412.
- Swap the order of
AlgHom.card_of_splitsandAlgHom.cardin FieldTheory/PrimitiveElement to avoid importing AlgebraicClosure. - Simplify the statements of two theorems in GroupTheory/CosetCover and deduce an easier-to-use form.
- Add two extensionality lemmas for AlgHom out of
Algebra.adjoin R sin RingTheory/Adjoin/Basic. - Add two lemmas to Minpoly/Field and golf
minpoly.eq_of_rootin FieldTheory/Adjoin.