norm_num extension for IsCoprime

This module defines a norm_num extension for IsCoprime over ℤ.

(While IsCoprime is defined over ℕ, since it uses Bezout's identity with ℕ coefficients it does not correspond to the usual notion of coprime.)

theorem Tactic.NormNum.int_not_isCoprime_helper (x : ℤ) (y : ℤ) (d : ℕ) (hd : x.gcd y = d) (h : d.beq 1 = false) : ¬IsCoprime x y

theorem Tactic.NormNum.isInt_isCoprime {x : ℤ} {y : ℤ} {nx : ℤ} {ny : ℤ} : Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → IsCoprime nx ny → IsCoprime x y

theorem Tactic.NormNum.isInt_not_isCoprime {x : ℤ} {y : ℤ} {nx : ℤ} {ny : ℤ} : Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → ¬IsCoprime nx ny → ¬IsCoprime x y

def Tactic.NormNum.proveIntIsCoprime (ex : Q(ℤ)) (ey : Q(ℤ)) : Q(IsCoprime «$ex» «$ey») ⊕ Q(¬IsCoprime «$ex» «$ey»)

Evaluates IsCoprime for the given integer number literals. Panics if ex or ey aren't integer number literals.

Equations

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

def Tactic.NormNum.evalIntIsCoprime : Mathlib.Meta.NormNum.NormNumExt

Evaluates the IsCoprime predicate over ℤ.

Equations

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