Commit 2023-06-24 07:10 4df50f9e

View on Github →

feat: port NumberTheory.Cyclotomic.Rat (#5417)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Cyclotomic/Rat.lean

added theorem IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime

added theorem IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow

added theorem IsCyclotomicExtension.Rat.discr_odd_prime'

added theorem IsCyclotomicExtension.Rat.discr_prime_pow'

added theorem IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'

added theorem IsCyclotomicExtension.Rat.discr_prime_pow_ne_two'

added theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime

added theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow

added theorem IsPrimitiveRoot.integralPowerBasis'_gen

added theorem IsPrimitiveRoot.integralPowerBasis_dim

added theorem IsPrimitiveRoot.integralPowerBasis_gen

added theorem IsPrimitiveRoot.power_basis_int'_dim

added theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen

added theorem IsPrimitiveRoot.subOneIntegralPowerBasis_gen