Theorems · Theorem · number theory

modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow

∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g : L ≃+* L) (p : ℕ) [inst_2 : Fact (Nat.Prime p)]
  [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] {i k : ℕ},
  k ≤ i → ↑p ^ k ∣ modularCyclotomicCharacter.aux g (p ^ i) - modularCyclotomicCharacter.aux g (p ^ k)

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFactHasEnoughRootsOfUnity