Mathlib Map

Theorems · Theorem · number theory

modularCyclotomicCharacter.spec

∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] {n : ℕ} [inst_2 : NeZero n]
  (hn : Nat.card ↥(rootsOfUnity n L) = n) (g : L ≃+* L) {t : Lˣ},
  t ∈ rootsOfUnity n L → g ↑t = ↑t ^ (↑((modularCyclotomicCharacter L hn) g)).val
Defined in
Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Cited by
1 results in Mathlib
Foundations
Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingIsDomainNeZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

cyclotomicCharacter.toFun_spec · cited by 1cyclotomicCharacter.toFun…DFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingMonoidHom · cited by 3629MonoidHomSubgroup · cited by 3593SubgroupUnits · cited by 2804UnitsIsDomain · cited by 2196IsDomainUnits.val · cited by 1966Units.valRingEquiv · cited by 1147RingEquivZMod · cited by 1024ZModNat.card · cited by 844Nat.cardZMod.val · cited by 159ZMod.valrootsOfUnity · cited by 118rootsOfUnitymodularCyclotomicCharacter.toFun · cited by 10modularCyclotomicCharacte…modularCyclotomicCharacter · cited by 6modularCyclotomicCharacterZMod.ringEquivCongr_val · cited by 3ZMod.ringEquivCongr_valmodularCyclotomicCharacter.sp…CITED BYCITES

Cites16

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
  • MonoidHomstatement · cited by 3,629
  • Subgroupstatement · cited by 3,593
  • Unitsstatement and proof · cited by 2,804
  • IsDomainstatement and proof · cited by 2,196
  • Units.valstatement and proof · cited by 1,966
  • RingEquivstatement and proof · cited by 1,147
  • ZModstatement · cited by 1,024
  • Nat.cardstatement and proof · cited by 844
  • ZMod.valstatement and proof · cited by 159
  • rootsOfUnitystatement and proof · cited by 118

Cited by1

Results whose statement or proof uses this declaration.