Commit 2023-06-09 06:37 62b6b1aa

View on Github →

feat: port FieldTheory.Normal (#4856)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.mem_roots_iff_aeval_eq_zero

Created Mathlib/FieldTheory/Normal.lean

added theorem AlgEquiv.liftNormal_commutes

added def AlgEquiv.restrictNormal

added def AlgEquiv.restrictNormalHom

added theorem AlgEquiv.restrictNormalHom_surjective

added theorem AlgEquiv.restrictNormal_commutes

added theorem AlgEquiv.restrictNormal_trans

added theorem AlgEquiv.restrict_liftNormal

added theorem AlgEquiv.transfer_normal

added theorem AlgHom.fieldRange_of_normal

added theorem AlgHom.liftNormal_commutes

added theorem AlgHom.normal_bijective

added def AlgHom.restrictNormal'

added def AlgHom.restrictNormal

added def AlgHom.restrictNormalAux

added theorem AlgHom.restrictNormal_commutes

added theorem AlgHom.restrictNormal_comp

added theorem AlgHom.restrict_liftNormal

added theorem IntermediateField.restrictScalars_normal

added def Normal.algHomEquivAut

added theorem Normal.exists_isSplittingField

added theorem Normal.isAlgebraic

added theorem Normal.isIntegral

added theorem Normal.of_algEquiv

added theorem Normal.of_isSplittingField

added theorem Normal.out

added theorem Normal.splits

added theorem Normal.tower_top_of_normal

added theorem isSolvable_of_isScalarTower

added theorem normalClosure.restrictScalars_eq_iSup_adjoin

added theorem normal_iff

Modified Mathlib/RingTheory/PowerBasis.lean