Regular primes

Main definitions

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

instance safe {p : ℕ+} : NumberField (CyclotomicField p ℚ)

Equations

• @safe = @safe.proof_1

instance safe' {p : ℕ+} : FiniteDimensional ℚ (CyclotomicField p ℚ)

Equations

• @safe' = @safe'.proof_1

instance CyclotomicField.classGroupFinite {p : ℕ+} : Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) })

Equations

• CyclotomicField.classGroupFinite = ClassGroup.fintypeOfAdmissibleOfFinite ℚ (CyclotomicField p ℚ) AbsoluteValue.absIsAdmissible

instance instFactLtNatInstLTNatOfNatInstOfNatNat {p : ℕ} [hp : Fact (Nat.Prime p)] : Fact (0 < p)

Equations

• @instFactLtNatInstLTNatOfNatInstOfNatNat = @instFactLtNatInstLTNatOfNatInstOfNatNat.proof_1

def IsRegularNumber (n : ℕ) [hn : Fact (0 < n)] : Prop

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

Equations

• IsRegularNumber n = Nat.Coprime n (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := n, property := (_ : 0 < n) } ℚ) }))

def IsRegularPrime (p : ℕ) [Fact (Nat.Prime p)] : Prop

The definition of regular primes.

Equations

• IsRegularPrime p = IsRegularNumber p

def IsBernoulliRegular (p : ℕ) [Fact (Nat.Prime p)] : Prop

A prime number is Bernoulli regular if it does not divide the numerator of any of the first p - 3 (non-zero) Bernoulli numbers

Equations

• IsBernoulliRegular p = ∀ (i : ℕ), i ∈ Finset.range ((p - 3) / 2) → ↑(bernoulli 2 * ↑i).num ≠ 0

def IsSuperRegular (p : ℕ) [Fact (Nat.Prime p)] : Prop

A prime is super regular if its regular and Bernoulli regular.

Equations

• IsSuperRegular p = (IsRegularNumber p ∧ IsBernoulliRegular p)

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

• One or more equations did not get rendered due to their size.

instance IsPrincipalIdealRing_of_IsCyclotomicExtension_two (L : Type u_1) [Field L] [CharZero L] [IsCyclotomicExtension {2} ℚ L] : IsPrincipalIdealRing { x // x ∈ NumberField.ringOfIntegers L }

Equations

• IsPrincipalIdealRing_of_IsCyclotomicExtension_two = IsPrincipalIdealRing_of_IsCyclotomicExtension_two.proof_1

instance instIsCyclotomicExtensionSingletonPNatSetInstSingletonSetOfNatRatCyclotomicFieldMkNatLtInstLTNatInstOfNatNatTwo_posToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringSemiringToPartialOrderStrictOrderedSemiringZeroLEOneClassOrderedSemiringSuccZeroTo_covariantClass_leftToOrderedAddCommMonoidFieldCommRingToCommRingToEuclideanDomainInstFieldCyclotomicFieldAlgebraRatToDivisionRingInstCharZeroCyclotomicFieldToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingInstFieldCyclotomicFieldTo_charZeroNumberField : IsCyclotomicExtension {2} ℚ (CyclotomicField { val := 2, property := (_ : 0 < 2) } ℚ)

Equations

• One or more equations did not get rendered due to their size.

instance instIsPrincipalIdealRingSubtypeCyclotomicFieldMkNatLtInstLTNatOfNatInstOfNatNatTwo_posToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringSemiringToPartialOrderStrictOrderedSemiringZeroLEOneClassOrderedSemiringSuccZeroTo_covariantClass_leftToOrderedAddCommMonoidRatFieldMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommRingToEuclideanDomainInstFieldCyclotomicFieldAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToRing : IsPrincipalIdealRing { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := 2, property := (_ : 0 < 2) } ℚ) }

Equations

• One or more equations did not get rendered due to their size.

theorem isRegularNumber_two : IsRegularNumber 2