Theorem IntermediateField.Lifts.exists_lift_of_splits'

Modification history

2024-01-11 20:30

Mathlib/FieldTheory/Adjoin.lean

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

Modified IntermediateField.Lifts.exists_lift_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.Lifts.exists_lift_of_splits'View on Github →