Mathlib v3 is deprecated. Go to Mathlib v4

Theorem gal_mul_is_solvable

Modification history

2022-02-08 12:43
src/field_theory/abel_ruffini.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified gal_mul_is_solvableView on Github →
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 gal_mul_is_solvableView on Github →