@[extern lean_int_div_exact]

def HexArith.Int.exactDiv (num denom : Int) : Int

Integer exact division without a proof argument on the value path.

Equations

• HexArith.Int.exactDiv num denom = num / denom

@[simp]

theorem HexArith.Int.exactDiv_zero (denom : Int) : exactDiv 0 denom = 0

theorem HexArith.Int.exactDiv_eq_divExact {num denom : Int} (h : denom ∣ num) : exactDiv num denom = num.divExact denom h

Under the divisibility invariant, exactDiv agrees with Int.divExact.