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.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 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) (checkIfModified : Bool) : 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.