# `norm_num` extension for integer div/mod and divides #

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

source
theorem Mathlib.Meta.NormNum.isInt_ediv_zero {a b r : ℤ} :
IsInt a r → IsNat b 0 → IsNat (a / b) 0
source
theorem Mathlib.Meta.NormNum.isInt_ediv {a b q m a' : ℤ} {b' r : ℕ} (ha : IsInt a a') (hb : IsNat b b') (hm : q * ↑b' = m) (h : ↑r + m = a') (h₂ : r.blt b' = true) :
IsInt (a / b) q
source
theorem Mathlib.Meta.NormNum.isInt_ediv_neg {a b q q' : ℤ} (h : IsInt (a / -b) q) (hq : -q = q') :
IsInt (a / b) q'
source
theorem Mathlib.Meta.NormNum.isNat_neg_of_isNegNat {a : ℤ} {b : ℕ} (h : IsInt a (Int.negOfNat b)) :
IsNat (-a) b
source
def Mathlib.Meta.NormNum.evalIntDiv :
NormNumExt

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

source
def Mathlib.Meta.NormNum.evalIntDiv.core (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt «$a» «$na»)) (b : Q(ℤ)) (nb : Q(ℕ)) (pb : Q(IsNat «$b» «$nb»)) :
ℤ × (q : Q(ℤ)) × Q(IsInt («$a» / «$b») «$q»)

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

Instances For

source
theorem Mathlib.Meta.NormNum.isInt_emod_zero {a b r : ℤ} :
IsInt a r → IsNat b 0 → IsInt (a % b) r
source
theorem Mathlib.Meta.NormNum.isInt_emod {a b q m a' : ℤ} {b' r : ℕ} (ha : IsInt a a') (hb : IsNat b b') (hm : q * ↑b' = m) (h : ↑r + m = a') (h₂ : r.blt b' = true) :
IsNat (a % b) r
source
theorem Mathlib.Meta.NormNum.isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) :
IsNat (a % b) r
source
def Mathlib.Meta.NormNum.evalIntMod :
NormNumExt

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

source
def Mathlib.Meta.NormNum.evalIntMod.go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt «$a» «$na»)) (b : Q(ℤ)) :
Result b → Option (Result q(«$a» % «$b»))

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

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Meta.NormNum.evalIntMod.go a na za pa b x✝ = none

Instances For

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

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

Instances For

source
theorem Mathlib.Meta.NormNum.isInt_dvd_true {a b a' b' c : ℤ} :
IsInt a a' → IsInt b b' → a'.mul c = b' → a ∣ b
source
theorem Mathlib.Meta.NormNum.isInt_dvd_false {a b a' b' : ℤ} :
IsInt a a' → IsInt b b' → (b'.emod a' != 0) = true → ¬a ∣ b
source
def Mathlib.Meta.NormNum.evalIntDvd :
NormNumExt

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