Commit 2021-01-27 08:41 e95928c0

View on Github →

feat(field_theory/normal): Restrict to normal subfield (#5845) Now that we know that splitting fields are normal, it makes sense to move the results of #5562 to normal.lean.

Estimated changes