Theorem IsGalois.of_separable_splitting_field

Modification history

2026-06-18 19:42

Mathlib/FieldTheory/Galois/Basic.lean

refactor(FieldTheory/*): swap imports of `IsSepClosed` and `SeparableClosure` (#40777) …

Modified IsGalois.of_separable_splitting_field View on Github →

2023-06-16 05:40

Mathlib/FieldTheory/Galois.lean

feat: port FieldTheory.Galois (#5115)

Added IsGalois.of_separable_splitting_field View on Github →