Commit 2026-08-12 12:56 ea2822d3

View on Github →

feat(FieldTheory): generalise Separable.of_algHom (#40700) From BrauerGroup

Estimated changes

Modified Mathlib/FieldTheory/Separable.lean

modified theorem Algebra.IsSeparable.of_algHom

modified theorem IsSeparable.of_algHom