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 Mathlib.Meta.NormNum.int_not_isCoprime_helper (x y : ℤ) (d : ℕ) (hd : x.gcd y = d) (h : d.beq 1 = false) : ¬IsCoprime x y

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

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

def Mathlib.Meta.NormNum.proveIntIsCoprime (ex 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 Mathlib.Meta.NormNum.evalIntIsCoprime : NormNumExt

Evaluates the IsCoprime predicate over ℤ.

Equations

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