Mathlib Map

Theorems · Theorem · number theory

modularCyclotomicCharacter.comp

∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g h : L ≃+* L),
  modularCyclotomicCharacter.toFun n (g * h) =
    modularCyclotomicCharacter.toFun n g * modularCyclotomicCharacter.toFun n h
Defined in
Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Cited by
0 results in Mathlib
Foundations
Depth 146 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.

modularCyclotomicCharacter' · cited by 2modularCyclotomicCharacte…DFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingRing · cited by 7463RingMonoid · cited by 3887MonoidSubgroup · cited by 3593SubgroupUnits · cited by 2804Unitsmul_comm · cited by 2262mul_commIsDomain · cited by 2196IsDomainUnits.val · cited by 1966Units.valRingEquiv · cited by 1147RingEquivZMod · cited by 1024ZModNat.card · cited by 844Nat.cardCharP · cited by 478CharPorderOf · cited by 324orderOfNat.cast_mul · cited by 309Nat.cast_mulmodularCyclotomicCharacter.co…CITED BYCITES

Cites26

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

  • DFunLike.coeproof · cited by 62,936
  • CommRingstatement and proof · cited by 17,173
  • Ringproof · cited by 7,463
  • Monoidproof · cited by 3,887
  • Subgroupstatement · cited by 3,593
  • Unitsstatement and proof · cited by 2,804
  • mul_commproof · cited by 2,262
  • IsDomainstatement and proof · cited by 2,196
  • Units.valproof · cited by 1,966
  • RingEquivstatement and proof · cited by 1,147
  • ZModstatement and proof · cited by 1,024
  • Nat.cardstatement and proof · cited by 844

Cited by1

Results whose statement or proof uses this declaration.