Theorem IntermediateField.minpoly_eq

Modification history

2024-08-21 07:40
Mathlib/FieldTheory/IntermediateField/Algebraic.lean
chore: split FieldTheory/IntermediateField (#15692)
Modified IntermediateField.minpoly_eqView on Github →
2023-09-18 04:21
Mathlib/FieldTheory/IntermediateField.lean
chore: replace `minpoly.eq_of_algebraMap_eq` by `algebraMap_eq` (#7228) …
Modified IntermediateField.minpoly_eqView on Github →
2023-05-23 11:55
Mathlib/FieldTheory/IntermediateField.lean
feat: port FieldTheory.IntermediateField (#4258)
Added IntermediateField.minpoly_eqView on Github →