Documentation

Mathlib.Tactic.NormNum.Parity

norm_num extensions for Even and Odd #

In this file we provide norm_num extensions for Even n and Odd n, where n : ℕ or n : ℤ.

source
🔸 coverage
def Mathlib.Meta.NormNum.evalEven :
NormNumExt

norm_num extension for Even.

Works for ℕ and ℤ.

Equations
    Instances For
      source
      🔸 coverage
      def Mathlib.Meta.NormNum.evalOdd :
      NormNumExt

      norm_num extension for Odd.

      Works for ℕ and ℤ.

      Equations
        Instances For