Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one

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

Let (x : 𝓞 K). Then we have that λ divides one amongst x, x - 1 and x + 1.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldIsCyclotomicExtension