Documentation

Mathlib.Tactic.NormNum.ModEq

norm_num extensions for Nat.ModEq and Int.ModEq #

In this file we define norm_num extensions for a ≡ b [MOD n] and a ≡ b [ZMOD n].

source
def Mathlib.Meta.NormNum.evalNatModEq :
NormNumExt

norm_num extension for Nat.ModEq.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Meta.NormNum.evalIntModEq :
    NormNumExt

    norm_num extension for Int.ModEq.

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