Documentation

Mathlib.Tactic.NormNum.IsCoprime

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) :
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.
Instances For

    Evaluates the IsCoprime predicate over .

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