Commit 2025-01-23 18:20 27deb239

View on Github →

refactor(FieldTheory/Normal): Split file (#20724) This PR splits FieldTheory/Normal. In particular, the proof of normal iff splitting field is now in FieldTheory/Normal/Basic.

Estimated changes

deleted theorem AlgEquiv.transfer_normal
deleted theorem AlgHom.normal_bijective
deleted theorem Normal.isIntegral
deleted theorem Normal.of_algEquiv
deleted theorem Normal.out
deleted theorem Normal.splits
deleted theorem normal_iff
added theorem Normal.isIntegral
added theorem Normal.of_algEquiv
added theorem Normal.out
added theorem Normal.splits
added theorem normal_iff