Theorem IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraic

Modification history

2024-01-10 19:15
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
feat (FieldTheory/Adjoin): generalize `IntermediateField.exists_algHom_of_splits` (#9392) …
Added IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraicView on Github →