Mathlib Map

Theorems · Theorem · number theory

cyclotomicCharacter.toZModPow_toFun

∀ {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)] (n : ℕ),
  (PadicInt.toZModPow n) (cyclotomicCharacter.toFun p g) = ↑((modularCyclotomicCharacter L ⋯) g)
Defined in
Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Cited by
2 results in Mathlib
Foundations
Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingIsDomainFactHasEnoughRootsOfUnity
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

cyclotomicCharacter.toFun_spec · cited by 1cyclotomicCharacter.toFun…cyclotomicCharacter.toZModPow · cited by 1cyclotomicCharacter.toZMo…DFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingRingHom · cited by 10189RingHomMonoidHom · cited by 3629MonoidHomUnits · cited by 2804UnitsFact · cited by 2726FactIsDomain · cited by 2196IsDomainNat.Prime · cited by 2059Nat.PrimeUnits.val · cited by 1966Units.valRingEquiv · cited by 1147RingEquivZMod · cited by 1024ZModPadicInt · cited by 179PadicIntHasEnoughRootsOfUnity · cited by 56HasEnoughRootsOfUnitymap_intCast · cited by 45map_intCastPadicInt.toZModPow · cited by 17PadicInt.toZModPowcyclotomicCharacter.toZModPow…CITED BYCITES

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement and proof · cited by 62,936
  • CommRingstatement and proof · cited by 17,173
  • RingHomstatement · cited by 10,189
  • MonoidHomstatement · cited by 3,629
  • Unitsstatement · cited by 2,804
  • Factstatement and proof · cited by 2,726
  • IsDomainstatement and proof · cited by 2,196
  • Nat.Primestatement and proof · cited by 2,059
  • Units.valstatement and proof · cited by 1,966
  • RingEquivstatement and proof · cited by 1,147
  • ZModstatement · cited by 1,024
  • PadicIntstatement and proof · cited by 179

Cited by2

Results whose statement or proof uses this declaration.