Mathlib v3 is deprecated. Go to Mathlib v4

Theorem splits_X_pow_sub_one_of_X_pow_sub_C

Modification history

2021-03-19 09:01
src/field_theory/abel_ruffini.lean
feat(field_theory/abel_ruffini): solvable by radicals implies solvable Galois group (#6631) …
Added splits_X_pow_sub_one_of_X_pow_sub_CView on Github →