Theorem IsIntegral.minpoly_splits_tower_top'

Modification history

2024-08-09 00:58

Mathlib/RingTheory/Adjoin/Field.lean

chore: backports for leanprover/lean4#4814 (part 24) (#15520)

Modified IsIntegral.minpoly_splits_tower_top'View on Github →

2024-01-10 19:15

Mathlib/RingTheory/Adjoin/Field.lean

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

Added IsIntegral.minpoly_splits_tower_top'View on Github →