Commit 2024-01-06 13:21 39e97562

View on Github →

feat: Cyclic extensions are kummer. (#9368)

Estimated changes

Modified Mathlib/FieldTheory/KummerExtension.lean

added theorem exists_root_adjoin_eq_top_of_isCyclic

added theorem irreducible_X_pow_sub_C_of_root_adjoin_eq_top

added theorem isCyclic_tfae

added theorem isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top

Modified Mathlib/FieldTheory/Minpoly/Field.lean

added theorem minpoly_algEquiv_toLinearMap

added theorem minpoly_algHom_toLinearMap

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem IsOfFinOrder.isUnit

added def IsOfFinOrder.unit

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.HasEigenvector.pow_apply

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem linearIndependent_algHom_toLinearMap'

added theorem linearIndependent_algHom_toLinearMap