FltRegular.NumberTheory.Cyclotomic.CyclRat

instance Ring.toSubtractionMonoid {S : Type u_1} [Ring S] :

Equations

Ring.toSubtractionMonoid = inferInstance

theorem exists_int_sub_pow_prime_dvd (p : ℕ+) {A : Type u_1} [CommRing A] [IsCyclotomicExtension {p} ℤ A] [hp : Fact (Nat.Prime ↑p)] (a : A) :

∃ m, a ^ ↑p - ↑m ∈ Ideal.span {↑↑p}

source

instance aaaa (p : ℕ+) (L : Type u) [Field L] [CharZero L] [IsCyclotomicExtension {p} ℚ L] [Fact (Nat.Prime ↑p)] :

IsCyclotomicExtension {p} ℤ { x // x ∈ NumberField.ringOfIntegers L }

Equations

aaaa = aaaa.proof_1

source

def fltIdeals (p : ℕ+) [Fact (Nat.Prime ↑p)] (x : ℤ) (y : ℤ) {η : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} :

η ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) } → Ideal { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }

The principal ideal generated by x + y ζ^i for integer x and y

Equations

fltIdeals p x y x = Ideal.span {↑x + η * ↑y}

Instances For

source

theorem mem_fltIdeals {p : ℕ+} [Fact (Nat.Prime ↑p)] (x : ℤ) (y : ℤ) {η : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη : η ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) :

↑x + η * ↑y ∈ fltIdeals p x y hη

source

theorem Ideal.le_add {S : Type u_1} [CommRing S] (a : Ideal S) (b : Ideal S) (c : Ideal S) (d : Ideal S) (hab : a ≤ b) (hcd : c ≤ d) :

a + c ≤ b + d

source

theorem not_coprime_not_top {S : Type u_1} [CommRing S] (a : Ideal S) (b : Ideal S) :

¬IsCoprime a b ↔ a + b ≠ ⊤

source

instance a1 {p : ℕ+} :

IsGalois ℚ (CyclotomicField p ℚ)

Equations

@a1 = @a1.proof_1

source

instance a2 {p : ℕ+} :

FiniteDimensional ℚ (CyclotomicField p ℚ)

Equations

@a2 = @a2.proof_1

source

instance a3 {p : ℕ+} :

NumberField (CyclotomicField p ℚ)

Equations

@a3 = @a3.proof_1

source

theorem nth_roots_prim {p : ℕ+} [Fact (Nat.Prime ↑p)] {η : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη : η ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hne1 : η ≠ 1) :

IsPrimitiveRoot η ↑p

source

theorem prim_coe {p : ℕ+} (ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hζ : IsPrimitiveRoot ζ ↑p) :

IsPrimitiveRoot ↑ζ ↑p

source

theorem zeta_sub_one_dvb_p {p : ℕ+} [Fact (Nat.Prime ↑p)] (ph : 5 ≤ p) {η : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη : η ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hne1 : η ≠ 1) :

1 - η ∣ ↑↑p

source

theorem one_sub_zeta_prime {p : ℕ+} [Fact (Nat.Prime ↑p)] (ph : 5 ≤ p) {η : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη : η ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hne1 : η ≠ 1) :

Prime (1 - η)

source

theorem diff_of_roots {p : ℕ+} [hp : Fact (Nat.Prime ↑p)] (ph : 5 ≤ p) {η₁ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} {η₂ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hdiff : η₁ ≠ η₂) (hwlog : η₁ ≠ 1) :

∃ u, η₁ - η₂ = ↑u * (1 - η₁)

source

theorem diff_of_roots2 {p : ℕ+} [Fact (Nat.Prime ↑p)] (ph : 5 ≤ p) {η₁ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} {η₂ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hdiff : η₁ ≠ η₂) (hwlog : η₁ ≠ 1) :

∃ u, η₂ - η₁ = ↑u * (1 - η₁)

source

instance arg {p : ℕ+} :

IsDedekindDomain { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }

Equations

@arg = @arg.proof_1

source

instance instAddCommGroupSubtypeCyclotomicFieldRatFieldMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommRingToEuclideanDomainInstFieldCyclotomicFieldAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegers {p : ℕ+} :

AddCommGroup { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }

Equations

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

source

instance instAddCommMonoidSubtypeCyclotomicFieldRatFieldMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommRingToEuclideanDomainInstFieldCyclotomicFieldAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegers {p : ℕ+} :

AddCommMonoid { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }

Equations

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

source

theorem fltIdeals_coprime2_lemma {p : ℕ+} [Fact (Nat.Prime ↑p)] (ph : 5 ≤ p) {x : ℤ} {y : ℤ} {η₁ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} {η₂ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y) (hp2 : ¬↑↑p ∣ x + y) (hwlog : η₁ ≠ 1) :

fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤

source

theorem fltIdeals_coprime2 {p : ℕ+} [Fact (Nat.Prime ↑p)] (ph : 5 ≤ p) {x : ℤ} {y : ℤ} {η₁ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} {η₂ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y) (hp2 : ¬↑↑p ∣ x + y) (hwlog : η₁ ≠ 1) :

IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)

source

theorem aux_lem_flt {p : ℕ+} [Fact (Nat.Prime ↑p)] {x : ℤ} {y : ℤ} {z : ℤ} (H : x ^ ↑p + y ^ ↑p = z ^ ↑p) (caseI : ¬↑↑p ∣ x * y * z) :

¬↑↑p ∣ x + y

source

theorem fltIdeals_coprime {p : ℕ+} (hpri : Nat.Prime ↑p) (p5 : 5 ≤ p) {x : ℤ} {y : ℤ} {z : ℤ} (H : x ^ ↑p + y ^ ↑p = z ^ ↑p) {η₁ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} {η₂ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }} (hxy : IsCoprime x y) (hη₁ : η₁ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField p ℚ) }) (hdiff : η₁ ≠ η₂) (caseI : ¬↑↑p ∣ x * y * z) :

let_fun this := (_ : Fact (Nat.Prime ↑p)); IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)

source

theorem dvd_last_coeff_cycl_integer {p : ℕ+} {L : Type u} [Field L] [CharZero L] [IsCyclotomicExtension {p} ℚ L] [hp : Fact (Nat.Prime ↑p)] {ζ : { x // x ∈ NumberField.ringOfIntegers L }} (hζ : IsPrimitiveRoot ζ ↑p) {f : Fin ↑p → ℤ} (hf : ∃ i, f i = 0) {m : ℤ} (hdiv : ↑m ∣ Finset.sum Finset.univ fun j => f j • ζ ^ ↑j) :

m ∣ f { val := Nat.pred ↑p, isLt := (_ : Nat.pred ↑p < ↑p) }

source

theorem dvd_coeff_cycl_integer {p : ℕ+} {L : Type u} [Field L] [CharZero L] [IsCyclotomicExtension {p} ℚ L] (hp : Nat.Prime ↑p) {ζ : { x // x ∈ NumberField.ringOfIntegers L }} (hζ : IsPrimitiveRoot ζ ↑p) {f : Fin ↑p → ℤ} (hf : ∃ i, f i = 0) {m : ℤ} (hdiv : ↑m ∣ Finset.sum Finset.univ fun j => f j • ζ ^ ↑j) (j : Fin ↑p) :

m ∣ f j