Theorems · Definition · number theory
DirichletCharacter.Even
{S : Type u_2} → [inst : CommRing S] → {m : ℕ} → DirichletCharacter S m → PropA Dirichlet character is even if its value at -1 is 1.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- DirichletCharacterstatement and proof · cited by 161
Cited by15
Results whose statement or proof uses this declaration.
- DirichletCharacter.rootNumberproof · cited by 3
- DirichletCharacter.gammaFactorproof · cited by 3
- DirichletCharacter.Even.to_funstatement and proof · cited by 3
- DirichletCharacter.even_or_oddstatement and proof · cited by 2
- DirichletCharacter.not_even_and_oddstatement and proof · cited by 2
- DirichletCharacter.Even.LFunction_neg_two_mul_nat_add_onestatement and proof · cited by 1
- DirichletCharacter.Even.gammaFactor_defstatement and proof · cited by 1
- DirichletCharacter.Odd.not_evenstatement · cited by 1
- DirichletCharacter.rootNumber_modOneproof · cited by 1
- DirichletCharacter.LFunction_eq_completed_div_gammaFactorproof · cited by 0
- DirichletCharacter.Even.LFunction_neg_two_mul_natstatement and proof · cited by 0
- DirichletCharacter.Even.eval_negstatement and proof · cited by 0