Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one

∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K},
  hζ.toInteger - 1 ∣ x - 1 → (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1

If λ divides x - 1, then λ ^ 4 divides x ^ 3 - 1.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Cited by

2 results in Mathlib

Foundations

Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldIsCyclotomicExtension