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

Equations

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

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

Equations

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