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
    Instances For
      source
      def Mathlib.Meta.NormNum.evalIntModEq :
      NormNumExt

      norm_num extension for Int.ModEq.

      Equations
        Instances For