Theorems · Definition · number theory
DirichletCharacter.Odd
{S : Type u_2} → [inst : CommRing S] → {m : ℕ} → DirichletCharacter S m → PropA Dirichlet character is odd if its value at -1 is -1.
- Cited by
- 11 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 by11
Results whose statement or proof uses this declaration.
- DirichletCharacter.Odd.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.Odd.gammaFactor_defstatement and proof · cited by 1
- DirichletCharacter.Odd.not_evenstatement and proof · cited by 1
- DirichletCharacter.LFunction_eq_completed_div_gammaFactorproof · cited by 0
- DirichletCharacter.Even.not_oddstatement · cited by 0
- DirichletCharacter.IsPrimitive.completedLFunction_one_subproof · cited by 0
- DirichletCharacter.Odd.LFunction_neg_two_mul_nat_sub_onestatement and proof · cited by 0
- DirichletCharacter.Odd.eval_negstatement and proof · cited by 0
- DirichletCharacter.Odd.toUnitHom_eval_neg_onestatement and proof · cited by 0