Theorem IntermediateField.exists_algHom_of_splits'

Modification history

2025-11-20 19:42

Mathlib/FieldTheory/Extension.lean

feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)

Modified IntermediateField.exists_algHom_of_splits'View on Github →

2024-01-11 20:30

Mathlib/FieldTheory/Adjoin.lean

chore: split IntermediateField.Lifts out of FieldTheory/Adjoin (#9647)

Modified IntermediateField.exists_algHom_of_splits'View on Github →

2024-01-10 19:15

Mathlib/FieldTheory/Adjoin.lean

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

Added IntermediateField.exists_algHom_of_splits'View on Github →