Theorem Algebra.isSeparable_of_separable_splitting_field

Modification history

2026-06-18 19:42
Mathlib/FieldTheory/SeparableClosure.lean
refactor(FieldTheory/*): swap imports of `IsSepClosed` and `SeparableClosure` (#40777) …
Added Algebra.isSeparable_of_separable_splitting_fieldView on Github →