Mathlib v3 is deprecated. Go to Mathlib v4

Theorem normal.of_is_splitting_field

Modification history

2023-05-08 23:09
src/field_theory/normal.lean
feat(*): generalise+add algebraic instances (#18947) …
Modified normal.of_is_splitting_fieldView on Github →
2022-02-08 12:43
src/field_theory/normal.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified normal.of_is_splitting_fieldView on Github →
2021-01-29 19:10
src/field_theory/normal.lean
feat(field_theory/polynomial_galois_group): New file (#5861) …
Modified normal.of_is_splitting_fieldView on Github →
2021-01-20 19:25
src/field_theory/normal.lean
feat(field_theory/normal): Splitting field is normal (#5768) …
Added normal.of_is_splitting_fieldView on Github →