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 : ℤ.

norm_num extension for Even.

Works for and .

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    norm_num extension for Odd.

    Works for and .

    Instances For