def Int.Linear.Poly.gcdAll : Poly → Nat

Equations

• (Int.Linear.Poly.num k').gcdAll = k'.natAbs
• (Int.Linear.Poly.add k' v p_1).gcdAll = Int.Linear.Poly.gcdAll.go k'.natAbs p_1

def Int.Linear.Poly.gcdAll.go (k : Nat) (p : Poly) : Nat

Equations

• Int.Linear.Poly.gcdAll.go k (Int.Linear.Poly.num k') = if (k == 1) = true then k else k.gcd k'.natAbs
• Int.Linear.Poly.gcdAll.go k (Int.Linear.Poly.add k' v p_2) = if (k == 1) = true then k else Int.Linear.Poly.gcdAll.go (k.gcd k'.natAbs) p_2

def Int.Linear.Poly.gcdCoeffs' : Poly → Nat

Equations

• (Int.Linear.Poly.num k').gcdCoeffs' = 1
• (Int.Linear.Poly.add k' v p_1).gcdCoeffs' = Int.Linear.Poly.gcdCoeffs'.go k'.natAbs p_1

def Int.Linear.Poly.gcdCoeffs'.go (k : Nat) (p : Poly) : Nat

Equations

• Int.Linear.Poly.gcdCoeffs'.go k (Int.Linear.Poly.num k') = if (k == 1) = true then k else k
• Int.Linear.Poly.gcdCoeffs'.go k (Int.Linear.Poly.add k' v p_2) = if (k == 1) = true then k else Int.Linear.Poly.gcdCoeffs'.go (k.gcd k'.natAbs) p_2

def Lean.Meta.Simp.Arith.Int.simpEq? (e : Expr) : MetaM (Option (Expr × Expr))

Equations

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

def Lean.Meta.Simp.Arith.Int.simpLe? (e : Expr) : MetaM (Option (Expr × Expr))

Equations

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

def Lean.Meta.Simp.Arith.Int.simpRel? (e : Expr) : MetaM (Option (Expr × Expr))

Equations

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

def Lean.Meta.Simp.Arith.Int.simpDvd? (e : Expr) : MetaM (Option (Expr × Expr))

Equations

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

def Lean.Meta.Simp.Arith.Int.simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr))

Equations

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