Commit 2023-06-22 09:14 5a55608d

View on Github →

feat: port NumberTheory.Cyclotomic.Basic (#5335)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Cyclotomic/Basic.lean

added def CyclotomicField

added theorem CyclotomicRing.adjoin_algebra_injective

added theorem CyclotomicRing.algebraBase_injective

added theorem CyclotomicRing.eq_adjoin_primitive_root

added def CyclotomicRing

added theorem IsAlgClosed.isCyclotomicExtension

added theorem IsCyclotomicExtension.adjoin_primitive_root_eq_top

added theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots

added theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic

added def IsCyclotomicExtension.algEquiv

added theorem IsCyclotomicExtension.empty

added theorem IsCyclotomicExtension.equiv

added theorem IsCyclotomicExtension.finite

added theorem IsCyclotomicExtension.finiteDimensional

added theorem IsCyclotomicExtension.finite_of_singleton

added theorem IsCyclotomicExtension.iff_adjoin_eq_top

added theorem IsCyclotomicExtension.iff_singleton

added theorem IsCyclotomicExtension.iff_union_of_dvd

added theorem IsCyclotomicExtension.iff_union_singleton_one

added theorem IsCyclotomicExtension.integral

added theorem IsCyclotomicExtension.isGalois

added theorem IsCyclotomicExtension.isSplittingField_X_pow_sub_one

added theorem IsCyclotomicExtension.neZero

added theorem IsCyclotomicExtension.ne_zero'

added theorem IsCyclotomicExtension.numberField

added theorem IsCyclotomicExtension.of_union_of_dvd

added theorem IsCyclotomicExtension.singleton_one

added theorem IsCyclotomicExtension.singleton_one_of_algebraMap_bijective

added theorem IsCyclotomicExtension.singleton_one_of_bot_eq_top

added theorem IsCyclotomicExtension.singleton_zero_of_bot_eq_top

added theorem IsCyclotomicExtension.splits_X_pow_sub_one

added theorem IsCyclotomicExtension.splits_cyclotomic

added theorem IsCyclotomicExtension.splitting_field_cyclotomic

added theorem IsCyclotomicExtension.subsingleton_iff

added theorem IsCyclotomicExtension.trans

added theorem IsCyclotomicExtension.union_left

added theorem IsCyclotomicExtension.union_right

added theorem IsPrimitiveRoot.adjoin_isCyclotomicExtension

Modified Mathlib/RingTheory/Adjoin/Basic.lean