Commit 2023-12-30 19:16 ba4be74a

View on Github →

feat: Kummer extensions are cyclic. (#9119)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Units/Hom.lean

added theorem Units.map_injective

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.nthRoots_zero_right

Created Mathlib/FieldTheory/KummerExtension.lean

added def AdjoinRootXPowSubCEquivToRootsOfUnity

added theorem Algebra.adjoin_root_eq_top_of_isSplittingField

added theorem IntermediateField.adjoin_root_eq_top_of_isSplittingField

added theorem Polynomial.separable_X_pow_sub_C_of_irreducible

added theorem X_pow_sub_C_eq_prod

added theorem X_pow_sub_C_splits_of_isPrimitiveRoot

added def adjoinRootXPowSubCEquiv

added theorem adjoinRootXPowSubCEquiv_root

added theorem adjoinRootXPowSubCEquiv_symm_eq_root

added def autAdjoinRootXPowSubC

added def autAdjoinRootXPowSubCEquiv

added theorem autAdjoinRootXPowSubCEquiv_root

added theorem autAdjoinRootXPowSubCEquiv_symm_smul

added def autAdjoinRootXPowSubCHom

added theorem autAdjoinRootXPowSubC_root

added def autEquivRootsOfUnity

added theorem autEquivRootsOfUnity_apply_rootOfSplit

added theorem autEquivRootsOfUnity_smul

added def autEquivZmod

added theorem autEquivZmod_symm_apply_intCast

added theorem autEquivZmod_symm_apply_natCast

added theorem finrank_of_isSplittingField_X_pow_sub_C

added theorem isCyclic_of_isSplittingField_X_pow_sub_C

added theorem isGalois_of_isSplittingField_X_pow_sub_C

added theorem isSplittingField_AdjoinRoot_X_pow_sub_C

added theorem ne_zero_of_irreducible_X_pow_sub_C'

added theorem ne_zero_of_irreducible_X_pow_sub_C

added theorem rootOfSplitsXPowSubC_pow

added theorem root_X_pow_sub_C_eq_zero_iff

added theorem root_X_pow_sub_C_ne_zero'

added theorem root_X_pow_sub_C_ne_zero

added theorem root_X_pow_sub_C_ne_zero_iff

added theorem root_X_pow_sub_C_pow

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem MulEquiv.subgroupCongr_apply

added theorem MulEquiv.subgroupCongr_symm_apply

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem IsPrimitiveRoot.card_nthRoots

added theorem IsPrimitiveRoot.card_nthRoots_one

added theorem IsPrimitiveRoot.injOn_pow

added theorem IsPrimitiveRoot.injOn_pow_mul

added theorem IsPrimitiveRoot.isUnit_unit'

added theorem IsPrimitiveRoot.isUnit_unit

added theorem IsPrimitiveRoot.map_rootsOfUnity

added theorem IsPrimitiveRoot.nthRoots_eq

modified theorem IsPrimitiveRoot.nthRoots_nodup

added theorem IsPrimitiveRoot.nthRoots_one_nodup

added def rootsOfUnityEquivOfPrimitiveRoots

added theorem rootsOfUnityEquivOfPrimitiveRoots_symm_apply

Modified docs/references.bib