Theorem IsSepClosed.surjective_comp_algebraMap_of_isSeparable

Modification history

2024-11-17 19:21

Mathlib/FieldTheory/IsSepClosed.lean

chore: use AlgHom.restrictDomain (#19116) …

Deleted IsSepClosed.surjective_comp_algebraMap_of_isSeparable View on Github →

2024-01-10 19:15

Mathlib/FieldTheory/IsSepClosed.lean

feat (FieldTheory/Adjoin): generalize `IntermediateField.exists_algHom_of_splits` (#9392) …

Added IsSepClosed.surjective_comp_algebraMap_of_isSeparable View on Github →