instance DirichletCharacter.instDecidablePredOddOfDecidableEq_formalConjecturesForMathlib {S : Type u_1} [DecidableEq S] [CommRing S] {m : ℕ} : DecidablePred Odd

Equations

• ψ.instDecidablePredOddOfDecidableEq_formalConjecturesForMathlib = decidable_of_iff (ψ (-1) = -1) ⋯

instance DirichletCharacter.instDecidablePredEvenOfDecidableEq_formalConjecturesForMathlib {S : Type u_1} [DecidableEq S] [CommRing S] {m : ℕ} : DecidablePred Even

Equations

• ψ.instDecidablePredEvenOfDecidableEq_formalConjecturesForMathlib = decidable_of_iff (ψ (-1) = 1) ⋯