Theorems · Theorem · number theory

sub_one_dvd_natCast_of_pow_eq_one

∀ {n : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A], ζ ^ n = 1 → ζ ≠ 1 → ζ - 1 ∣ ↑n

If ζ ^ n = 1 and ζ ≠ 1, then ζ - 1 divides n. This does not require ζ to be a primitive root of unity, only a root of unity different from 1.

Defined in

Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain