Theorem IntermediateField.Lifts.exists_lift_of_splits'

Modification history

2024-11-23 06:30

Mathlib/FieldTheory/Extension.lean

feat(FieldTheory): minimal polynomials determine an algebraic extension (Isaacs 1980) (#18412) …

Modified IntermediateField.Lifts.exists_lift_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.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 →