Regular primes

Main definitions

• IsRegularNumber: a natural number n is regular if n is coprime with the cardinal of the class group.

def IsRegularNumber (n : ℕ) : Prop

A natural number n is regular if n is coprime with the cardinal of the class group.

Equations

• IsRegularNumber n = n.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers (CyclotomicField n ℚ))))

def IsRegularPrime (p : ℕ) : Prop

The definition of regular primes.

Equations

• IsRegularPrime p = IsRegularNumber p

noncomputable def cyclotomicFieldTwoEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [IsCyclotomicExtension {2} K L] : L ≃ₐ[K] K

The second cyclotomic field is equivalent to the base field.

Equations

• cyclotomicFieldTwoEquiv K L = (Polynomial.IsSplittingField.algEquiv L (Polynomial.cyclotomic 2 K)).trans (Polynomial.IsSplittingField.algEquiv K (Polynomial.cyclotomic 2 K)).symm

instance IsPrincipalIdealRing_of_IsCyclotomicExtension_two (L : Type u_3) [Field L] [CharZero L] [IsCyclotomicExtension {2} ℚ L] : IsPrincipalIdealRing (NumberField.RingOfIntegers L)

instance instIsCyclotomicExtensionSingletonNatSetOfNatRatCyclotomicField_leanPool : IsCyclotomicExtension {2} ℚ (CyclotomicField 2 ℚ)

instance instIsPrincipalIdealRingRingOfIntegersCyclotomicFieldOfNatNatRat_leanPool : IsPrincipalIdealRing (NumberField.RingOfIntegers (CyclotomicField 2 ℚ))

theorem isRegularPrime_two : IsRegularPrime 2

theorem isRegularPrime_three : IsRegularPrime 3