Theorems · Theorem · number theory

cyclotomicCharacter.toFun_apply

∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] (g : L ≃+* L)
  [inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)],
  cyclotomicCharacter.toFun p g = PadicInt.ofIntSeq (fun n => modularCyclotomicCharacter.aux g (p ^ n)) ⋯

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFactHasEnoughRootsOfUnity