Theorem Algebra.IsSeparable.iff_of_equiv_equiv

Modification history

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