Documentation

Mathlib.Tactic.NormNum.DivMod

norm_num extension for integer div/mod and divides #

This file adds support for the %, /, and (divisibility) operators on to the norm_num tactic.

theorem Mathlib.Meta.NormNum.isInt_ediv {a : } {b : } {q : } {m : } {a' : } {b' : } {r : } (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (hm : q * b' = m) (h : r + m = a') (h₂ : r.blt b' = true) :
theorem Mathlib.Meta.NormNum.isInt_ediv_neg {a : } {b : } {q : } {q' : } (h : Mathlib.Meta.NormNum.IsInt (a / -b) q) (hq : -q = q') :

The norm_num extension which identifies expressions of the form Int.ediv a b, such that norm_num successfully recognises both a and b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Mathlib.Meta.NormNum.evalIntDiv.core (a : Q()) (na : Q()) (za : ) (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) (b : Q()) (nb : Q()) (pb : Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb»)) :
    × (q : Q()) × Q(Mathlib.Meta.NormNum.IsInt («$a» / «$b») «$q»)

    Given a result for evaluating a b in where b > 0, evaluate a / b.

    Instances For
      theorem Mathlib.Meta.NormNum.isInt_emod {a : } {b : } {q : } {m : } {a' : } {b' : } {r : } (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (hm : q * b' = m) (h : r + m = a') (h₂ : r.blt b' = true) :

      The norm_num extension which identifies expressions of the form Int.emod a b, such that norm_num successfully recognises both a and b.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Mathlib.Meta.NormNum.evalIntMod.go (a : Q()) (na : Q()) (za : ) (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) (b : Q()) :

        Given a result for evaluating a b in , evaluate a % b.

        Equations
        Instances For
          def Mathlib.Meta.NormNum.evalIntMod.core (a : Q()) (na : Q()) (za : ) (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) (b : Q()) (nb : Q()) (pb : Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb»)) :
          (r : Q()) × Q(Mathlib.Meta.NormNum.IsNat («$a» % «$b») «$r»)

          Given a result for evaluating a b in where b > 0, evaluate a % b.

          Instances For
            theorem Mathlib.Meta.NormNum.isInt_dvd_true {a : } {b : } {a' : } {b' : } {c : } :
            Mathlib.Meta.NormNum.IsInt a a'Mathlib.Meta.NormNum.IsInt b b'a'.mul c = b'a b
            theorem Mathlib.Meta.NormNum.isInt_dvd_false {a : } {b : } {a' : } {b' : } :
            Mathlib.Meta.NormNum.IsInt a a'Mathlib.Meta.NormNum.IsInt b b'(b'.emod a' != 0) = true¬a b

            The norm_num extension which identifies expressions of the form (a : ℤ) ∣ b, such that norm_num successfully recognises both a and b.

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