Theorem IsSeparable.of_integral

Modification history

2024-09-19 08:44

Mathlib/FieldTheory/Separable.lean

feat(FieldTheory/Separable): Add lemmas of elementwise `IsSeparable` (#14404) …

Added IsSeparable.of_integral View on Github →