Theorem IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraic

Modification history

2024-11-17 19:21

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

chore: use AlgHom.restrictDomain (#19116) …

Deleted IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraic View on Github →

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_isAlgebraic View on Github →